Petrify: Petri-net Based Analysis of
Concurrency Properties in Java Bytecode Akshatha Shenoy1 [0009−0004−2439−1656] and Carlo A. Furia1 [0000−0003−1040−3201] Software Institute, USI Università della Svizzera italiana, Lugano, Switzerland
arXiv:2607.00830v1 [cs.SE] 1 Jul 2026
bugcounting.net
Abstract. The landscape of automated formal verification is populated by techniques that make prominently different trade-offs: some focus on expressiveness and precision, supporting the verification of complex properties; others favor scalability and practicality, so that they are applicable to larger programs using different features. This paper presents Petrify, a novel automated verification technique for concurrency properties that achieves a distinctive trade-off. Petrify encodes the semantics of Java bytecode programs into Petri nets (PNs), which can be analyzed by state-of-the-art model checking tools such as LoLA. As our experiments demonstrate, Petrify’s approach offers an interesting combination of expressiveness and practicality: PNs are a fairly precise encoding of the concurrent behavior of programs; at the same time, Petrify’s PN encoding is succinct, so that its analysis remains quite insensitive to parameter size. Another practical benefit of targeting bytecode is that jPetrify, the prototype tool that implements the Petrify technique, is applicable to programs written in any version of Java and even a subset of Kotlin (another language that compiles to Java bytecode) while other similar tools are limited to older versions of Java. While this paper’s experiments focus on analyzing fundamental properties like deadlock, Petrify’s approach lends itself to be extended to other kinds of concurrency analysis, which we plan to tackle in future work.
1
Introduction
Every automated formal program analysis technique has to contend with the expressiveness vs. scalability trade-off. Techniques that favor expressiveness support precisely verifying all sorts of user-defined properties, but may struggle to analyze large programs. In contrast, techniques that target scalability are based on bespoke abstractions that approximate only specific hardcoded properties, but are applicable to realistic-size programs. In the domain of concurrent verification, for example, software model checkers (e.g., Java Pathfinder [10]) favor expressiveness as they support temporal logic specifications and other kinds of program annotations, and can analyze path conditions precisely. In contrast, custom static analyzers that focus on a single property (e.g., data races for Infer’s RacerD [1] or deadlocks for JaDA [19]) are usually more efficient but cannot verify other kinds of properties and may suffer from imprecision. Another important dimension of practicality for any formal verification tool is language support. Most analysis techniques work at the source-code level, which entails that they may struggle to keep up with the evolution of modern languages. Consider, again, the example of Java: tools like Pathfinder and JaDA were developed for earlier versions of Java, and hence
cannot analyze programs that include recently introduced features—even if the features themselves do not affect the concurrent behavior. All the more so, applying a verification technique to work on a (subset of a) different language (even one that is similar to Java) is usually onerous—in terms of both adapting the technique and developing a suitable implementation toolchain. This paper presents Petrify, a program analysis technique for concurrent Java programs that explores a novel trade-off between expressiveness, scalability, and language support. Petrify relies on two key ideas. First, it encodes the concurrent behavior of a Java program as a Petri net. Thanks to recent advances in their algorithmic verification, PNs have become an appealing abstract model of concurrent computation, which combines a high expressiveness with highly optimized model-checking tools. Second, Petrify translates directly from Java bytecode, rather than working at the source code level. This makes it a technique that is not tied too closely to a specific version of Java, and even works for programs written in (an imperative subset of) Kotlin—another language that compiles to Java bytecode—which provides an additional element of flexibility and practicality. In our experiments to demonstrate Petrify’s capabilities, we implemented it in a tool called jPetrify, and applied it to detect deadlocks in 36 Java and 3 Kotlin programs taken or adapted from various benchmarks. Although our prototype implementation of jPetrify currently only supports a limited number of properties out of the box, the experiments demonstrated some of its strengths, which complement other state-of-the-art tools such as Java Pathfinder and JaDA. In particular, jPetrify is applicable to Java programs written in any version of the language, whereas other tools usually cannot process versions more recent than Java 11. In addition, Petrify’s abstractions are insensitive to the parameter size, so that jPetrify scales up to examples that heavier, more precise tools cannot handle. Contributions. The paper makes the following main contributions: i) Petrify: a novel technique to analyze concurrency properties of bytecode programs based on a flowand context-sensitive, path-insensitive encoding of bytecode programs into Petri nets. ii) jPetrify: an implementation of Petrify based on the Soot static analyzer and the LoLA Petri net model checker. iii) An experimental evaluation of jPetrify on 39 programs. iv) The implementation of jPetrify and the experimental artifacts are available [27]. For lack of space, some technical details and examples have been moved to the appendix. The main text remains self-contained, while focusing on key high-level details.
2
An Overview of Petrify
Fig. 1a shows a simple concurrent Java program with two threads thread_12 and thread_21 that try to acquire a lock on variables lock1 and lock2. It is easy to see that the program will deadlock if the two threads interleave their lock acquisition operations, leading to a state where t_12 has a lock on lock1, t_21 has a lock on lock2, and each thread waits for the other thread to release the lock it is holding. Let’s describe how Petrify analyzes this program to find the deadlock scenario. Petrify works on bytecode (produced by the Java compiler), rather than on source Java code. One advantage of targeting bytecode is that we can support any Java version, since new language features (e.g., Fig. 1a’s instance main method and unnamed class, which were introduced in Java 21 and still are preview features) are desugared into a stable set of bytecode instructions by the compiler. 2
1 void
main() {
Object lock1 = new Object();
2
Object lock2 = new Object(); Runnable r_12 = () -> { synchronized (lock1) { synchronized (lock2) {}}};
3 4
Runnable r_21 = () -> { synchronized (lock2) { synchronized (lock1) {}}}; Thread t_12 = new Thread(lock_12);
5 6
8
Thread t_21 = new Thread(lock_21); t_12.start();
9
t_21.start();
7
10 }
(a) A two-threaded Java program that may deadlock. entrymain :
ℓ0 : ℓ1 : ℓ2 : ℓ3 : ℓ4 : ℓ5 : exitmain :
def main begin write lock1 write lock2 write t_12 write t_21 fork r_12 t_12 fork r_21 t_21 end
def r_12 entryr_12 : begin ℓ6 : acquire lock1 ℓ7 : acquire lock2 ℓ8 : release lock2 ℓ9 : release lock1 exitr_12 : end
def r_21 entryr_21 : begin ℓ10 : acquire lock2 ℓ11 : acquire lock1 ℓ12 : release lock1 ℓ13 : release lock2 exitr_21 : end
(b) Petrify’s translation of Fig. 1a’s program into the rb intermediate language. t_12
t_12
exit
exit
t_12
t_12 t_12
t_12 lock2 t_21 lock2
m 𝑡0
ℓ9
m 𝑡0
ℓ9
ℓ8
ℓ8
ℓ7
ℓ7
ℓ6
entry
ℓ6
entry m 𝑡0 m 𝑡0
• entry
entry
t_21
t_21
exit
exit
ℓ0
ℓ0
ℓ13
ℓ1
ℓ13
ℓ1
ℓ12
ℓ2
ℓ2
ℓ12
ℓ3
ℓ11
ℓ3
ℓ11
ℓ4
ℓ4
ℓ10
ℓ5
ℓ10
ℓ5
exit
lock1 t_21
exit
t_21
t_21
entry
entry
lock1
(c) Petrify’s encoding of Fig. 1b’s rb program as a Petri net. To reduce clutter, the arrows connecting transitions ℓ6–9 and ℓ10–13 to the four places , , , are shortened and rely on colors to indicate the connected place.
Fig. 1: A simple concurrent Java program, and Petrify’s encoding in rb and as a Petri net. Petrify first translates the input bytecode program into the rb program shown in Fig. 1b. rb is an intermediate language that is flow- and context-sensitive but pathinsensitive; hence, it represents an approximationof the bytecode program’s executions. We introduced rb to reduce the semantic gap between bytecode and Petri nets, which simplifies the design of the overall translation and also reasoning about its correctness. In this example, rb captures all aspects of concurrent behavior without information loss. Then, Petrify encodes the semantics of Fig. 1b’s rb program into the Petri net (PN) in Fig. 1c. Petrify supports the PN format used by state-of-the-art analyzers such as LoLA [31], so that its output can be fed to these tools to analyze any properties of interest. To check the presence of deadlocks, Petrify augments the output PN with additional “monitoring” places and transitions (now shown in Fig. 1c for simplicity) and a suitable temporal logic formula. With this input, LoLA quickly finds a PN execution that corresponds to Fig. 1a’s deadlock. As you can glean from Fig. 1c, the structure of the PN is clearly modular. The central chain of nodes (circular “places” and square “transition” in PN terminology) encodes the control flow of the main function, whereas the top and bottom chains correspond to the anonymous methods (lambdas) executed by threads t_12 and t_21 respectively. The
3
arrows connecting transitions ℓ4 and ℓ5 to the entry places of t_12 and t_21 represent the starting points of the threads parallel to main. The modular structure of Petrify’s PN encoding also helps map back an error trace given by the PN analyzer to an execution of the original Java program.
3
Related Work
There is a vast amount of research on detecting concurrency programming errors. For space constraints, we focus on techniques and tools that are applicable to Java and are currently available; as for any kind of program analysis, they can be broadly classified in static or dynamic, and according to their expressiveness vs. scalability. Static techniques are usually sound but imprecise. Deductive verification offers high expressiveness, as it can analyze user-defined complex properties; however, it requires a significant amount of human effort, as programs must be annotated with detailed formal specifications and additional assertions such as invariants. VerCors [2] and VeriFast [11] are two prominent examples of deductive verifiers for Java, both supporting annotations written in a combination of JML [20] and separation logic. VerCors offers a higher degree of automation, as it relies on the Viper intermediate verifier [26] to discharge verification conditions, while VeriFast supports interactive correctness proofs. Model checking is a popular verification technique based on analyzing (finite-)state models against temporal-logic properties. Tools like JPF (Java Pathfinder) [10], JayHorn [14], JBMC [5], and JMC [13] are software model checkers: they encode the semantics of a Java program using a state model that can be analyzed by a model checker such as Spin [30]. This provides a high degree of automation, while still supporting user-defined properties (usually expressible in temporal logic). Petrify follows a similar approach, but it leverages Petri nets (instead of less expressive automata models) to naturally model several aspects of a program’s concurrent behavior. A key issue when designing an analysis based on model checking is that the full semantics of a (Java) program is generally infinite-state. Some tools (e.g., JPF, JBMC, JMC) perform a bounded exploration of the infinite program state; hence, they are powerful testing tools, but are not sound in general. JPF, in particular, is a mature analysis framework based on a custom controllable version of the Java virtual machine; it can systematically or randomly explore execution paths and different thread interleavings. Symbolic JPF (SPF) performs the state exploration symbolically (using a form of symbolic execution), so that it is systematic and satisfies complex coverage criteria. Other techniques build a finitely-analyzable over-approximation of a program’s state space, which loses precision but retains soundness. Techniques like Infer’s RacerD [6,1] (based on separation logic and bi-abduction), Checkmate [8] (based on abstract interpretation) and Chord [15] (an unsound, precise technique based on context-sensitive analyses) are all different applications of static analysis to detect data races. JaDA [19] offers deadlock detection for (a subset of) Java bytecode; it uses typing rules to define an infinite-state abstract model of the program’s lock dependencies; the model is analyzable by means of a fixpoint decision algorithm. Petrify also builds, by means of a dataflow analysis, an approximation of a Java program’s executions, which it encodes as a finitely-analyzable Petri net. 4
Jimple ::= Method∗
RB ::= Proc∗
Method ::= method Id : Type∗ → Type {Instr∗ }
Proc ::= def Id begin Cmd∗ end Cmd ::= skip |
Instr ::= noop | goto Label | if Var Label | switch Var (Var : Label)
∗
|
goto Label
| jump Label Label |
| write Var |
Var := Expr | return Var | return |
read Var
monitor_enter Var
acquire Var
| monitor_exit Var
Expr ::= Var ⊕ Var | ⊙Var | Const | Call
| release Var |
fork Id Thread
∗
call Id
(a) Syntax of Jimple.
(b) Syntax of rb.
Call ::= invoke Id Var
| join Thread |
Fig. 2: Syntax of the intermediate representations used by Petrify.
Petri nets are a classic model of concurrency. To our knowledge, they have been historically mainly used to build abstract, high-level models, to encode the semantics of core concurrency properties (e.g., causal atomicity [7]) and primitives (e.g., synchronization through conditional variables [4]). In our work, we leverage the recent advances in model-checking tools for Petri nets [3,31,16] and use them as back-end of jPetrify. Dynamic analysis has become more popular in recent years to detect concurrency bugs such as deadlocks [29], data races [28,18], and linearizability [17,21] and atomicity [25,24] violations. While such techniques do not offer soundness, they are practical (i.e., since they are based on executing a program, they support all language features) and scalable (e.g., they analyze a trace in linear time). Soundness vs. precision. On paper, static and dynamic analysis offer complementary advantages and disadvantages: static techniques overapproximate program behavior, and hence their results are sound (exhaustive) but imprecise; dynamic techniques underapproximate program behavior, and hence their results are precise (no false alarms) but unsound. In practice, the boundary between soundness and precision is somewhat fuzzy, and even static techniques are very often unsound in certain cases [23], because they may not fully support certain language features due to practical concerns. As we will discuss in Sec. 5, Petrify follows a similar approach of being “mostly” sound and “reasonably” precise: i) Petrify’s implementation does not (fully) support certain Java language features; thus, the analysis results may be unsound for programs that use those features. ii) Petrify relies on an alias analysis to identify possibly shared lock and thread variables; when the alias analysis results are insufficiently precise, Petrify’s own analysis may in turn become unsound or imprecise. Ultimately, the practicality of Petrify in analyzing concurrent programs is established with Sec. 6’s experimental evaluation, which highlights its capabilities and limitations, also in comparison to other similar concurrency analysis tools.
4
Preliminaries: Jimple Bytecode, rb, and Petri nets
Petrify encodes the concurrent dataflow semantics of a JVM bytecode program as a Petri net. This section introduces the intermediate representations used by Petrify.
5
4.1 The Jimple Bytecode Representation Rather than working directly with JVM bytecode, Petrify uses Soot’s Jimple bytecode representation: a typed bytecode form that abstracts several low-level details and incorporates static information. Fig. 2a outlines the main constructs of Jimple, using a simplified abstract syntax. Before going through it, we point out that Jimple uses an SSA (static single assignment) form; thus, any complex expression ((𝑣 0 ⊕1 𝑣 1 ) ⊕2 𝑣 2 ) · · · ⊕𝑛 𝑣 𝑛 ) becomes a sequence of assignments to local variables 𝑟 1 := 𝑣 0 ⊕1 𝑣 1 , 𝑟 2 := 𝑟 1 ⊕2 𝑣 2 , . . . , 𝑟 𝑛 := 𝑟 𝑛−1 ⊕𝑛 𝑣 𝑛 , such that 𝑟 𝑛 stores the value of the whole expression. Thus, Jimple instructions generally only take variables (not expressions) as arguments. A Jimple program is a collection of methods, with at least one main method that corresponds to the program’s entry point. A Method has a name, a typed signature, and a body consisting of a sequence of instructions, which include: i) Control flow instructions: unconditional (goto) and conditional (if, switch) jumps to a location with a given label; return to the caller. ii) Assignment instructions perform any kind of expression evaluation using the SSA form discussed above. iii) Monitor instructions correspond to the synchronization when entering (monitor_enter) and exiting a synchronized block. iv) Call instructions are also only used in the right-hand side of an assignment. For simplicity, invoke represents all five variants of call instructions (static, virtual, etc.) available in bytecode. v) The noop instruction does nothing. Example 1. Fig. 1a’s example in Jimple consists of three methods: main, and two anonymous methods for the Runnable objects. Each synchronized block is a pair of matching monitor_enter and monitor_exit instructions. The other statements are different variants of invoke: invokespecial for the new creation expressions, and invokevirtual for the start() calls. ■ 4.2 The rb Intermediate Language To streamline the encoding of concurrent behavior into PNs, we introduce the rb intermediate language. In a nutshell, rb (short for Rock Bottom) is a simplified bytecodelike representation that captures flow- and context-sensitive information while abstracting away path-sensitive details. Syntax of rb. Fig. 2b outlines the syntax of rb. An RB program is a collection of procedures; like in Jimple (and Java) we assume that at least one main procedure exists. A Proc has a unique name, and a body consisting of a sequence of commands marked by begin and end. We also assume that each procedure 𝑝 also defines labels entry 𝑝 and exit 𝑝 marking, respectively, 𝑝’s unique entry and exit points. rb commands include: i) Control flow commands: unconditional (goto) and nondeterministic (jump) jumps; synchronously call a procedure 𝑝; spawn (fork) and wait for (join) a parallel thread 𝑡 running a procedure 𝑝. We assume that the thread identifiers in fork and join commands are distinct from all other identifiers, and that the main procedure runs on thread 𝑡 0 . ii) Synchronization commands to acquire and release a lock. iii) Access commands to read and write a variable. iv) The skip command does nothing. Given an rb program RB, 𝑇 denotes the set of all Thread identifiers, 𝑃 the set of all Procedure identifiers, 𝐵 the set of all Labels (we assume that each command has a unique label), and 𝑉 the set of all Variable names mentioned anywhere in the program. Semantics of rb. The state 𝑆 of an rb program is a set of tuples (𝑡, 𝑝, ℓ, 𝐾, 𝑅, 𝜏), where 𝑡 ∈ 𝑇 is a thread, 𝑝 ∈ 𝑃 is a procedure, ℓ ∈ 𝐵 is a command label, 𝐾 ⊆ 𝑉 is a set of 6
𝑠 = (𝑡, 𝑝, ℓ : 𝑐, 𝐿, 𝑅, ) ∈ 𝑆 𝑐 ∈ {skip, read 𝑣, write 𝑣} ′
𝑆 = 𝑆 \ {𝑠} ∪ {(𝑡, 𝑝, ℓ + 1, 𝐿, 𝑅, )} 𝑠 = (𝑡, 𝑝, exit 𝑝 , 𝐿, 𝑅 + [ℓ], ) ∈ 𝑆 ′
𝑠 = (𝑡, 𝑝, ℓ : call 𝑝 ′ , 𝐿, 𝑅, ) ∈ 𝑆 ′
𝑆 = 𝑆 \ {𝑠} ∪ {(𝑡, 𝑝 ′ , entry 𝑝′ , 𝐿, 𝑅 + [ℓ + 1], )}
ℓ ∈ 𝑝′
𝑠 = (𝑡, 𝑝, exit 𝑝 , 𝐿, ∅, ) ∈ 𝑆
′
′
𝑆 = 𝑆 \ {𝑠} ∪ {(𝑡, 𝑝, exit 𝑝 , 𝐿, ∅, é)}
𝑆 = 𝑆 \ {𝑠} ∪ {(𝑡, 𝑝 , ℓ, 𝐿, 𝑅, )} ′
𝑠 = (𝑡, 𝑝, ℓ : goto ℓ , 𝐿, 𝑅, ) ∈ 𝑆
𝑠 = (𝑡, 𝑝, ℓ : jump ℓ1 ℓ2 , 𝐿, 𝑅, ) ∈ 𝑆
𝑆 ′ = 𝑆 \ {𝑠} ∪ {(𝑡, 𝑝, ℓ ′ , 𝐿, 𝑅, )}
ℓ ′ ∈ {ℓ1 , ℓ2 }
𝑆 ′ = 𝑆 \ {𝑠} ∪ {(𝑡, 𝑝, ℓ ′ , 𝐿, 𝑅, )}
𝑠 = (𝑡, 𝑝, ℓ : acquire 𝑘, 𝐿, 𝑅, ) ∈ 𝑆 𝑘∉𝐿 ∀𝑡 ′ , 𝐿 ′ · (𝑡 ′ , _, _, 𝐿 ′ , _, _) ∈ 𝑆 ∧ 𝑡 ′ ≠ 𝑡 → 𝑘 ∉ 𝐿 ′
𝑠 = (𝑡, 𝑝, ℓ : release 𝑘, 𝐿, 𝑅, ) ∈ 𝑆
′
𝑘∈𝐿
′
𝑆 = 𝑆 \ {𝑠} ∪ {(𝑡, 𝑝, ℓ + 1, 𝐿 ∪ {𝑘 }, 𝑅, )}
𝑆 = 𝑆 \ {𝑠} ∪ {(𝑡, 𝑝, ℓ + 1, 𝐿 \ {𝑘 }, 𝑅, )} 𝑠 = (𝑡, 𝑝, ℓ : join 𝑡 ′ , 𝐿, 𝑅, ) ∈ 𝑆 𝑠′ = (𝑡 ′ , 𝑝 ′ , ℓ ′ , 𝐿 ′ , 𝑅 ′ , é) ∈ 𝑆
′ ′
𝑠 = (𝑡, 𝑝, ℓ : fork 𝑝 𝑡 , 𝐿, 𝑅, ) ∈ 𝑆 𝑆 ′ = 𝑆 \ {𝑠} ∪ {(𝑡, 𝑝, ℓ + 1, 𝐿, 𝑅, )} ∪ {(𝑡 ′ , 𝑝 ′ , entry 𝑝′ , ∅, ∅, )}
𝑆 ′ = 𝑆 \ {𝑠, 𝑠′ } ∪ {(𝑡, 𝑝, ℓ + 1, 𝐿, 𝑅, )}
Fig. 3: Operational semantics of rb. Each rule describes one step of evaluation 𝑆 ⇝ 𝑆 ′ when executing the command in the rule’s premise.
locked variables, 𝑅 ∈ 𝐵∗ is a sequence of procedure/label pairs, and 𝜏 ∈ { , é} is the thread’s termination state. Informally, such a tuple denotes a thread 𝑡 is ready to run command at label ℓ in procedure 𝑝, while holding locks 𝐾; 𝜏 denotes whether 𝑡 is still running ( ) or has terminated (é); and 𝑅 is a stack of return locations of pending calls. The initial state of an rb program is {(𝑡0 , main, entrymain , ∅, ∅, )}. Fig. 3 outlines an operational semantics of rb. Each rule shows how the state 𝑆 changes after executing a different command. Command skip simply continues execution of the thread 𝑡 to the next location ℓ + 1. Since rb abstracts away path-sensitive details, read and write behave exactly like skip. However, we still include them as separate commands since they allow us to model, in rb, the different interleavings of read and write operations in a JVM program, and behaviors that depend on them—such as data races. A call 𝑝 ′ command appends the return label ℓ + 1 to 𝑅 and continues executing the callee 𝑝 ′ from its entry point. Conversely, when a call terminates, the most recent return label is removed from 𝑅 and used as next command to execute. If the execution of a procedure 𝑝 reaches its exit point and 𝑅 is empty, this makes the whole thread 𝑡 terminate—denoted by 𝜏 = é. Both kinds of branching commands, goto and jump, change the current command label: goto does so unconditionally, whereas jump nondeterministically picks one of two possible labels. A thread 𝑡 can execute an acquire 𝑘 only if any other thread 𝑡 ′ is not holding a lock on 𝑘. In contrast, 𝑡 can execute a release 𝑘 without waiting, as long as it is currently holding a lock on 𝑘. Finally, a fork 𝑝 ′ 𝑡 ′ adds a new tuple (𝑡 ′ , 𝑝 ′ , entry 𝑝′ , ∅, ∅, ) to the state 𝑆, corresponding to a new thread 𝑡 ′ starting to execute procedure 𝑝 ′ . And a join 𝑡 ′ can execute only when thread 𝑡 ′ has terminated. Example 2. When Fig. 1b’s example rb program deadlocks, its state 𝑆 consists of the tuples: ( t_12, r_12, ℓ7 , {lock1}, [], ) , ( t_21, r_21, ℓ11 , {lock2}, [], ) , (𝑡0 , main, exitmain , ∅, [], é) . Neither ℓ7 nor ℓ11 can execute, because each thread state invalidates the other’s progress precondition. ■ 7
bytecode
property
Petri net
Deadlock.class
no deadlocks
Deadlock.pn
Soot
translation
T
rb
encoding
Deadlock.rb
E
LoLA □( 𝑝 → 𝑥)
Petrify
Ë
Jimple
é
Deadlock.jimple
Fig. 4: An overview of how Petrify works.
4.3
Petri Nets
A Petri net is a tuple (Π, Δ, 𝐴, 𝐼), where Π is a set of places, Δ is a set of transitions, 𝐴 ⊆ (Π × Δ) ∪ (Δ × Π) is a set of arcs connecting transitions to places and places to transitions, and 𝐼 : Π → N is an initial marking. The preset pre(𝛿) of a transition 𝛿 ∈ Δ is the set of places 𝜋 such that (𝜋, 𝛿) ∈ 𝐴; and the postset post(𝛿) is the set of places 𝜋 such that (𝛿, 𝜋) ∈ 𝐴. It is customary to picture a PN as a graph where places are circles, transitions are boxes, and arcs are arrows. Fig. 1 displays the running example’s PN using this notation; the black disks denote the net’s initial marking. Semantics of Petri nets. The state of a PN is a marking 𝑚 : Π → N, which denotes how many tokens 𝑚(𝜋) ≥ 0 each place 𝜋 ∈ Π holds. A transition 𝛿 ∈ Δ is enabled in a state 𝑚 whenever 𝑚(𝜋) > 0 for every place 𝜋 in pre(𝛿); in other words, all places that connect to 𝑡 are marked with at least one token. Whenever a transition 𝛿 is enabled, it can nondeterministically fire. If 𝛿 fires when the net is in state 𝑚, the new marking 𝑚 ′ is such that 𝑚 ′ ( 𝑝) = 𝑚( 𝑝) − 1 for every place 𝑝 ∈ pre(𝛿), and 𝑚 ′ ( 𝑝) = 𝑚( 𝑝) + 1 for every place 𝑝 ∈ post(𝛿). In other words, each place in 𝛿’s preset consumes one token, whereas each place in 𝛿’s postset acquires one additional token. If no transition is enabled in a marking 𝑚, the PN is in a deadlock. According to these definitions, a PN determines a set of possible firing sequences, corresponding to all sequences of transitions that can be triggered from the initial marking; each firing sequence corresponds to a sequence of markings 𝑚 0 ⊢ 𝑚 1 ⊢ . . . that begins with 𝑚 0 = 𝐼. The set of all firing/marking sequences denotes a PN’s semantics. Example 3. From its initial marking, Fig. 1c’s PN may reach the state where places ( t_12, ℓ7 ), ( t_21, ℓ11 ), ( t_12, lock1), ( t_21, lock2) are marked. From that state, no transition is possible: place ( t_12, lock2) is unmarked, which disables transition ( t_12, ℓ7 ); and place ( t_21, lock1) is unmarked, which disables transition ( t_21, ℓ11 ). ■
5
How Petrify Works
This section details Petrify’s approach. As outlined in Fig. 4, Petrify inputs a program 𝐽 in bytecode; precisely, it targets the Jimple format offered by the Soot static analyzer. Petrify translates 𝐽 into a corresponding rb program 𝑅 = T (𝐽) (Sec. 5.1); it then encodes 𝑅’s semantics as a Petri net 𝑃 = E (𝑅) (Sec. 5.2); it also produces suitable 8
temporal logic properties that can be passed as input, together with 𝑃, to a PN analyzer (e.g., LoLA) to detect concurrency issues (Sec. 5.3). 5.1
Translation of Jimple into rb
Given a bytecode program (in Jimple format) 𝐽, Petrify builds an rb program T (𝐽) = 𝑅 that captures a flow- and context-sensitive, path-insensitive approximation of 𝐽’s behavior. Modeling Aliasing. Consider any identifier 𝑛 that appears in 𝐽, including variable identifiers and method names. Let 𝜂(𝑛) denote 𝑛 expressed in a form that is unambiguous throughout the program: for example, if o.m denotes a method m of an object o of class O, 𝜂( o.m) denotes the fully qualified Ð name O.m with a suffix that distinguishes it from other overloaded variants. Let 𝜑 ≜ 𝜄 : Var {𝜂(𝜄)} denote the set of unique variable identifiers anywhere in 𝐽—which we’ll call “vars” for short. And let L denote the set of all locations in 𝐽. Petrify’s translation of bytecode uses a may point to analysis as follows. Let 𝜄 ∈ 𝜑 be a var used at location ℓ ∈ L in 𝐽; 𝜇 𝜄,ℓ ⊆ 𝜑 denotes the set of vars that may be aliased to 𝜄 according to the may point to analysis. The may-alias sets 𝜇 𝜄,ℓ determine an equivalence relation ≃+ ⊆ (𝜑 × L) × (𝜑 × L) among vars as follows: first, ≃ ⊆ (𝜑 × L) × (𝜑 × L) is the reflexive and symmetric relation defined by 𝜄1 , ℓ1 ≃ 𝜄2 , ℓ2 iff 𝜇 𝜄1 ,ℓ1 ∩ 𝜇 𝜄2 ,ℓ2 ≠ ∅; then, ≃+ is the transitive closure of ≃: 𝜄, ℓ ≃+ 𝜄′ , ℓ ′ iff there exist 𝜄1 , ℓ1 , . . . , 𝜄𝑛 , ℓ𝑛 such that 𝜄1 = 𝜄, ℓ1 = ℓ, 𝜄𝑛 = 𝜄′ , ℓ𝑛 = ℓ ′ , and 𝜄 𝑘 , ℓ𝑘 ≃ 𝜄 𝑘+1 , ℓ𝑘+1 for all 1 ≤ 𝑘 < 𝑛. Finally, let 𝛼(𝜄, ℓ) be a unique identifier that corresponds to the equivalence class of 𝜑 according to ≃+ that 𝜄, ℓ belongs to. Intuitively, 𝛼 assigns the same identifiers to any two vars in 𝐽 iff they may be aliased. rb Encoding. Tab. 1 outlines how Petrify translates Jimple statements into rb commands. Methods become procedures in rb, whose bodies get translated statement by statement. Conditional jumps (if and switch) become nondeterministic jumps (jump) in rb. This makes all control-flow paths in the Jimple program feasible in the rb program. Lock
acquisition statements (monitor_enter and monitor_exit) become the corresponding commands in rb (acquire and release). Finally, an assignment translates to a translation of its right-hand side expression, followed by a write to its target. The translation of non-call expressions is straightforward, as it corresponds to a read of the variables involved in the expression. An invoke translates to reads of its actual arguments and possibly its target, followed by a call to the rb procedure 𝜂(𝑜.𝑚) translating the called method 𝑜.𝑚. An exception is for calls of methods start and join on targets of type Thread: these become fork and join respectively. Soundness and Precision of the rb Encoding. The translation 𝑅 = T (𝐽) of 𝐽 is sound if the feasible execution paths in 𝑅 are a superset of those in 𝐽; conversely, an unsound translation may omit error paths that are possible in the original program. The translation is precise if the feasible execution paths in 𝑅 are a subset of those in 𝐽; conversely, an imprecise translation may include spurious error paths that are impossible in the original program. Let’s summarize how the translation scheme affects soundness and precision. i) Translating conditionals with nondeterministic jumps is sound but path-insensitive; hence, it generally involves a loss of precision. ii) The translation of lock operations in 𝐽 with acquire and release in 𝑅 is sound provided the lock is not used reentrantly. According to Fig. 3, rb does not allow a thread to acquire a lock on 𝑘 if it already holds a 9
rb translation T (𝑠)
Jimple 𝑠 method 𝑚 : 𝑡 1 . . . 𝑡 𝑛 → 𝑡 {𝐵}
def 𝜂(𝑚(𝑡 1 . . . 𝑡 𝑛 )) begin T (𝐵) end
𝑠1 ; 𝑠2
T (𝑠1 ); T (𝑠2 )
noop
skip
goto ℓ ′
goto ℓ¯′
if 𝑣 ℓ ′
read 𝛼(𝑣); jump ↷ ℓ¯′
switch 𝑣 (𝑣 1 : ℓ1 ) . . . (𝑣 𝑛 : ℓ𝑛 ) read 𝛼(𝑣); read 𝛼(𝑣 1 ); jump ↷ ℓ¯1 ; . . . ; read 𝛼(𝑣 𝑛 ); jump ↷ ℓ¯𝑛
𝑣 := 𝑒
T (𝑒); write 𝑣
return 𝑣
read 𝛼(𝑣); goto exit
return
goto exit
monitor_enter 𝑣 monitor_exit 𝑣
acquire 𝛼(𝑣)
𝑐 : Const 𝑣1 ⊕ 𝑣2 ⊙𝑣 invoke 𝑚 𝑜 𝑎 1 . . . 𝑎 𝑛 invoke start 𝑡 : Thread invoke join 𝑡 : Thread
release 𝛼(𝑣)
– read 𝛼(𝑣 1 ); read 𝛼(𝑣 1 ) read 𝛼(𝑣) read 𝛼(𝑣 1 ); . . . ; read 𝛼(𝑣 𝑛 ); read 𝛼(𝑜); call 𝜂(𝑜.𝑚) fork 𝜂(𝑡.start) 𝛼(𝑡) join 𝛼(𝑡)
Table 1: Translation T of Jimple instructions (top) and expressions (bottom) into rb commands. ℓ¯ denotes the location in the rb program that translates the instruction at location ℓ in the Jimple program; ↷ denotes the location of the next command; 𝜂(𝑛) denotes a unique form of identifier 𝑛; and 𝛼(𝑣) denotes a group of variables that may be aliased (see the text for a precise definition).
lock on it; thus, 𝑅 may omit such executions even if they are possible in 𝐽.1 iii) Petrify’s sound translation of call instructions depends on whether Soot can retrieve the body of the invoked closure object in invokedynamic instructions. This is possible in simple cases such as Fig. 1’s example, where invokedynamic is used to execute the Runnable lambdas r_12 and r_21; more complex instances of invokedynamic would become skip in 𝑅, which introduces unsoundness in general. iv) Other bytecode instructions that are not listed in Fig. 2a are currently unsupported by Petrify. The translation replaces any unsupported instruction 𝐼 with a skip, which means that 𝑅 doesn’t model 𝐼’s semantics. This may result in a loss of soundness or precision, depending on what execution paths the unsupported instruction does enable or block. v) Two variables 𝑣 1 , 𝑣 2 that may be aliased in 𝐽 are lumped together into a single variable 𝑣 = 𝛼(𝑣 1 ) = 𝛼(𝑣 2 ) in 𝑅; this may introduce a loss of soundness or, more commonly, precision. In practice, these limitations mainly imply the lack of support for certain program features. As our experiments in Sec. 6 show, Petrify remains applicable on broad range of Java programs following different concurrency patterns and features. While we plan to remove some limitations in future work, Petrify’s capabilities are consistent with the pragmatic approach of making program analysis work with realistic programs despite theoretical limitations [23]. Example 4. Fig. 1b shows Petrify’s rb translation of Fig. 1a; for simplicity, Fig. 1b omits the writes of variables r_12, r_21 (assignments on lines 4, 5) and the reads of variables r_12, r_21 (new expressions on lines 6, 7). Since the program does not have 1 Soundly modeling reentrant locks would require a stack-like counting mechanism, which goes
beyond the expressiveness of plain PNs; hence, it belongs to future work.
10
data-dependent path conditions, and there is no aliasing among variables, the translation to rb is sound and precise. The rb program consists of three procedures: main, and two Runnable anonymous functions that are each thread’s run() method. ■
𝑝𝑡 𝑝𝑡
𝑝𝑡
𝑝𝑡
𝑝𝑡
𝑝𝑡
𝑝′ 𝑡 ′
𝑝𝑡
exit 𝑝 ′
⊲⊳ ℓ
𝑝𝑡
𝑝𝑡
𝑝𝑡
𝑝𝑡
𝑝𝑡
ℓ → ℓ1 ℓ 𝑝𝑡
𝑝𝑡
ℓ
𝑝𝑡
𝑡𝑣 𝑝𝑡
𝑝𝑡
𝑝𝑡
ℓ
ℓ +1
ℓ
𝑝𝑡
ℓ ℓ ℓ +1 (e) 𝑝, 𝑡 , ℓ, 𝑟 : join 𝑡 ′
𝑡1 𝑣 𝑡2 𝑣 𝑡𝑛 𝑣 (f) 𝑝, 𝑡 , ℓ, 𝑟 : acquire 𝑣
𝑝𝑡 𝑝′ 𝑡
ℓ 𝑟1 𝑝𝑡
ℓ 𝑟1 𝑝𝑡
ℓ 𝑟2
ℓ 𝑟2
𝑝′ 𝑡 exit 𝑝 ′ ℓ
𝑝𝑡
ℓ
ℓ +1
𝑡1 𝑣 𝑡2 𝑣 𝑡𝑛 𝑣 (g) 𝑝, 𝑡 , ℓ, 𝑟 : release 𝑣 𝑝𝑡
𝑝𝑡
↩→ ℓ 𝑟1 𝑝𝑡
ℓ + 1 𝑟1 𝑝𝑡
↩→ ℓ 𝑟2
ℓ + 1 𝑟2
𝑝′ 𝑡
··· entry 𝑝 ′ ℓ
𝑝𝑡
···
··· ℓ ℓ ℓ +1 (d) 𝑝, 𝑡 , ℓ, 𝑟 : fork 𝑝 ′ 𝑡 ′
ℓ1
ℓ → ℓ2 ℓ2 (c) 𝑝, 𝑡 , ℓ, 𝑟 : jump ℓ1 ℓ2
𝑡𝑣
entry 𝑝 ′
𝑝𝑡
𝑝𝑡
ℓ ℓ ℓ′ (b) 𝑝, 𝑡 , ℓ, 𝑟 : goto ℓ ′
ℓ ℓ ℓ +1 (a) 𝑝, 𝑡 , ℓ, 𝑟 : skip, read 𝑣, write 𝑣
𝑝′ 𝑡 ′
𝑝𝑡
𝑝𝑡
↩→ ℓ
(h) 𝑝, 𝑡 , ℓ, 𝑟1,2 : call 𝑝 ′
Fig. 5: Fragments of Petri nets encoding rb commands.
5.2 Encoding of rb into Petri Nets Given an rb program 𝑅 with threads 𝑇, procedures 𝑃, labels 𝐵, and variables 𝑉, Petrify builds a PN 𝑁 = E (𝑅) = (Π, Δ, 𝐴, 𝐼) that over-approximates 𝑅’s semantics. The general idea is that when the command at location ℓ in procedure 𝑝 is ready to be executed by thread 𝑡, the corresponding place ( 𝑝, 𝑡, ℓ, 𝑟) is marked. The component 𝑟 denotes the caller location of 𝑝, which is ⊤ if 𝑝 is being executed on the main thread 𝑡 0 or on a freshly forked thread. Then, the corresponding transition ( 𝑝, 𝑡, ℓ, 𝑟) fires when the command executes; the transition’s postset denotes the commands that will be able to execute after 𝑐. With this approach, each combination of procedure, thread, and call site in 𝑅 corresponds to a set of connected nodes (places and transitions) in PN 𝑁. Formally, the set Π of places of PN 𝑁 includes, for every combination of location ℓ ∈ 𝐵, procedure 𝑝 ∈ 𝑃, thread 𝑡 ∈ 𝑇, and return label 𝑟 ∈ 𝐵 ∪ {⊤}: i) A place ( 𝑝, 𝑡, ℓ, 𝑟) if ℓ is a location in 𝑝 and one of the following holds: a) 𝑝 is main, 𝑡 is 𝑡 0 , and 𝑟 is ⊤; or b) there is a fork 𝑝 𝑡 somewhere in the program, and 𝑟 is ⊤; or c) there is a call 𝑝 at location 𝑟 ≠ ⊤ in the program. ii) A return place ( 𝑝, 𝑡, ↩→ ℓ) if ℓ is the location of a call 𝑝 command. iii) A join place ( 𝑝, 𝑡, ⊲⊳ ℓ, 𝑟) if ℓ is the location of a join 𝑡 ′ command. iv) A place (𝑡, 𝑣) for every variable 𝑣 ∈ 𝑉 such that there is an acquire 𝑣 or a release 𝑣 somewhere in the program. The set Δ of transitions includes, for every combination of location ℓ ∈ 𝐵, procedure 𝑝 ∈ 𝑃, thread 𝑡 ∈ 𝑇, and return label 𝑟 ∈ 𝐵 ∪ {⊤}: i) A transition ( 𝑝, 𝑡, ℓ, 𝑟) for every place ( 𝑝, 𝑡, ℓ, 𝑟) ∈ Π. ii) A return transition ( 𝑝, 𝑡, ↩→ ℓ, 𝑟) if ℓ is the location of a call 𝑝 command; iii) Two jump transitions ( 𝑝, 𝑡, ℓ → ℓ1 , 𝑟) and ( 𝑝, 𝑡, ℓ → ℓ2 , 𝑟) if ℓ is the location of a jump ℓ1 ℓ2 command. The initial marking 𝐼 has 11
one token in the place ( main, 𝑡0 , entrymain , ⊤)—the program’s unique entry point—and one token in each place (𝑡, 𝑣)—denoting that all locks are initially not held by any thread. For each command 𝑐 at location ℓ in procedure 𝑝 executed by thread 𝑡 with return location 𝑟, Fig. 5 shows the set 𝐴 of arcs that capture the command’s semantics. For readability, Fig. 5 omits the caller location 𝑟 for commands where it’s the same in all nodes (i.e., all commands but calls). For brevity, we only describe the most complex fragments: a) Command fork 𝑝 ′ 𝑡 ′ puts one token into the next location’s place, and one token into the forked thread’s entry point’s place ( 𝑝 ′ , 𝑡 ′ , entry 𝑝′ , 𝑟). This way, the forked thread’s computation can proceed in parallel to the forking thread’s. b) Conversely, join 𝑡 ′ can fire only when the exit transition ( 𝑝 ′ , 𝑡 ′ , exit 𝑝 ′ , 𝑟) of thread 𝑡 ′ fires (where 𝑝 ′ is the procedure that thread 𝑡 ′ is running). c) Command acquire 𝑣’s transition can fire only if all places (𝑡 ′ , 𝑣) are marked, denoting that no thread 𝑡 ′ holds a lock on 𝑣. When it fires, it puts back a token only in place (𝑡, 𝑣) to indicate that 𝑡 holds a lock on 𝑣. d) Command release 𝑣’s transition can fire only if place (𝑡, 𝑣) is marked, denoting that thread 𝑡 holds a lock on 𝑣. When it fires, it puts back a token in all places (𝑡 ′ , 𝑣), thus allowing other threads to acquire a lock on 𝑣. e) When the transition ( 𝑝, 𝑡, ℓ, 𝑟) of command call 𝑝 ′ fires, it puts a token in the callee’s entry place ( 𝑝 ′ , 𝑡, entry 𝑝′ , ℓ). Then, execution continues in the subnet corresponding procedure 𝑝 ′ called in thread 𝑡 at call site ℓ. Then, when transition ( 𝑝 ′ , 𝑡, exit 𝑝′ , ℓ) fires, signaling that the subnet’s execution has terminated, a token first goes into return place ( 𝑝 ′ , 𝑡, ↩→ ℓ); then one of the transitions ( 𝑝, 𝑡, ↩→ ℓ, 𝑟), for all possible callers of 𝑝 ′ , nondeterministically fires. Fig. 5h pictures two callers 𝑟 1 ≠ 𝑟 2 , where either of the return transitions ( 𝑝, 𝑡, ↩→ ℓ, 𝑟 𝑘 ), 𝑘 = 1, 2, may fire when the subnet terminates execution. This nondeterministic encoding is the only aspect of Petrify’s encoding of rb programs that loses precision: a PN cannot store an unbounded stack of return locations,2 and hence Petrify overapproximates it. Example 5. Fig. 1c shows the PN encoding of Fig. 1b and its initial marking. For readability, m abbreviates main, and we omit the caller in nodes since it’s ⊤ everywhere. The PN consists of three subnets, corresponding to the main (middle), r_12 (top), and r_21 (bottom) procedures; as well as four additional places ( t_𝑥𝑦, lock𝑚) that denote when t_𝑥𝑦 is holding a lock on lock𝑚. The arcs connecting main to the other subnets mark the spawning of each thread in the main thread 𝑡 0 ; and the colored arcs connecting transitions in the r_12 and r_21 subnets to the places ( t_𝑥𝑦, lock𝑚) with matching color synchronize the corresponding lock commands. ■ Lemma 1 (Correctness of Petri net encoding). Let 𝑃 be an rb program and 𝑁 = E (𝑃) its PN encoding defined by Petrify. Then, each sequence of state transitions according to 𝑃’s operational semantics corresponds to a marking sequences according to 𝑁’s semantics. Therefore, the semantics of 𝑁 is a sound over-approximation of 𝑃’s semantics. Proof. See appendix. 5.3 Encoding Properties and Implementation The trace semantics of the PN 𝑁 = T (E (𝐽)) built by Petrify is a path-insensitive approximation of the trace semantics of the input bytecode program 𝐽. Thus, 𝑁 can 2 PNs with inhibitor arcs would be able to simulate this without loss of precision; however, their
reachability problem becomes undecidable [9].
12
be analyzed with any standard PN analyzer, such as LoLA [31]. While this approach gives flexibility, since one may formalize a wide range of properties as formulas in the temporal logic supported by the analyzers, doing so requires some knowledge of how Petrify encodes programs into PNs. To improve Petrify’s usability, we built in support for common concurrency bugs: deadlock, livelock, and non-termination. We implemented the Petrify technique in a command-line tool called jPetrify. jPetrify inputs a bytecode program 𝐽, a property to be verified (a temporal logic formula, or absence of deadlocks, livelocks, or termination), uses Soot to analyze Jimple code and its control-flow, and produces a PN 𝑃 = E (T (𝐽)) as described in previous sections.
6
Experimental Evaluation
Evaluation goal. The goal of this experimental evaluation is to assess Petrify’s practical feasibility, highlighting its capabilities, limitations, and complementarity in comparison to other automated Java verification tools that can analyze similar concurrency properties. 6.1 Subjects and Setup Comparable tools. According to Sec. 3’s discussion, we focus on JPF (Java Pathfinder [10]) and JaDA [19] for the following reasons: i) they support checking (absence of) deadlocks out of the box—the same properties currently supported by jPetrify; ii) their public repositories (especially JaDA’s) include numerous examples of Java programs that demonstrate their capabilities in deadlock detection; iii) they represent two distinct approaches: JPF is based on model-checking, on top of which it implements an array of analysis techniques, whereas JaDA uses type-based static analysis and is specialized on deadlock detection; iv) their implementations have different levels of maturity: JPF is a mature tool with over 20 years of history, whereas JaDA is more recent and less polished, but with a ready-made, usable implementation. Our experiments are not meant as a direct comparison between jPetrify and these two tools; however, they will show that jPetrify works successfully on several examples that were designed for JPF and JaDA, indicating that our approach is viable and has potential, as well as its limitations compared to the state of the art. Subjects. We evaluated jPetrify’s capabilities on 39 example concurrent programs with shared locks. The leftmost part of Tab. 2 lists these programs, which belong to 7 groups: i) 2 are from JPF’s repository; ii) 14 are from JaDA’s repository [12]; iii) 2 are from the JaConTeBe [22] benchmarks; iv) 7 are variants of other examples: 2 are variants of programs in group JaDA (ClassicDeadlockN is a generalization of ClassicDeadlock, and PhilTable is a dining philosophers variant), and the other 5 use recent Java language features (up to Java 21); v) 11 are examples that specifically scale up the size and complexity of the verification problems by introducing nested loops, several threads, sequences of blocks, and unbounded recursion; vi) 3 are adaptations of other classic examples translated to Kotlin. We selected deadlock examples from JPF’s and JaDA’s repositories that don’t use features unsupported by jPetrify (especially arrays, which result in a major loss of precision); for the same reason, we refactored some of the JaDA examples to make them compatible with jPetrify without changing their behavior. As indicated in Tab. 2, 3 of the subjects are correct, and 36 include a concurrency (deadlock) bug. Therefore, the evaluation tests the tools’ capabilities both to precisely find bugs and to soundly verify correctness. 13
Challenges. Although most benchmark programs are relatively small in terms of lines, methods, or classes, they are far from trivial, and introduce various kinds of challenges to even state-of-the-art tools. In particular: i) Group variants uses language features (sealed classes, records, etc.) that have only been introduced in recent versions of Java; for approaches that work on the source level (like JPF and JaDA), supporting new language features is a major challenge that often goes beyond “mere” engineering. Notably, program VirtualThreads specifically targets a new concurrency feature of Java that jPetrify supports out of the box. On the other hand, program PhilTable uses a lot of aliased references, which challenge the tools’ abstraction of this feature. ii) Programs in group size feature different forms of complex control flow, which challenges the scalability of concurrency analysis: unbounded recursive synchronous calls (RecUnbounded, Chordv2); recursive thread spawning and joining (RecJoin); thread synchronization with unbounded loops (WhileCnt2N2T), deeply nested calls (Interleaving), and nested locking of many lock variables (Nested200T2); and an 8-thread generalization of the dining philosophers problem (DiningP8T). The remaining programs in this group feature behaviors that challenge concurrency analysis with complex dependency patterns (InnerThreads, JoinUnderLock, RecursiveJoinUnderLockDeadlock), such as circular waiting between parent and child threads, or require a context-sensitive analysis (DeeperContextDeadlock). Setup. We ran each example with jPetrify, JPF, and JaDA with 15-minute timeout; we classify a tool’s output as: i) success Ë if it correctly detects a deadlock or establishes that there is none; ii) false negative − if it misses an existing deadlock; iii) false positive + if it reports a spurious bug; iv) time out/out of memory ; v) failure due to unsupported features ○. All experiments ran on an Apple Macbook M3 Max with 36 GB RAM and macOS 15.6.1. jPetrify used Soot 4.6.0 and LoLA 2.0; JPF commit 0f2f2 used Java 11; the JaDA tool was run through its website3 since it is not available for download. 6.2 Results Performance. Tab. 2 shows that jPetrify’s encoding is succinct, with 2.4 (6624/2738) places per source line of code on average. Also as a result of this succinctness, verification is fast in most examples, typically taking under a second. In contrast, generating the PN encoding from bytecode takes significantly more time; however, most of the generation time (3.8 minutes per subject) is taken by Soot to extract from bytecode the information needed for the rb encoding, whereas jPetrify’s actual encoding is much faster (4.2 seconds per subject). The overall end-to-end performance of jPetrify is acceptable, but there are clear margins for improvement, in particular as we invest more time into optimizing its bottleneck interaction with Soot. It is also encouraging that the two outliers (Nested200T2 and especially PhilTable) that took considerably more time resulted in larger-than-average PN models that similarly challenged encoding and verification; in other words, they are intrinsically more complex examples. We did not collect the running time of JPF or JaDA: a proper comparison of performance would require controlled experimental conditions (not possible for JaDA whose implementation is not open source), and would be of limited interest for a prototype tool like jPetrify. jPetrify correctly verified (detecting a deadlock or confirming that none exists) 38 examples. The lone exception is PhilTable, where Soot’s alias analysis induces an 3 http://jada.cs.unibo.it/
14
group JPF
JaDA
benchmarks
variants
size
Kotlin total average
name
exp loc classes methods | PN |
soot [s]
enc [s]
ver outcome [s] jPe JPF JaDA
BankTransfer DiningPhil
18 40
2 3
4 3
91 133
175.9 212.1
0.5 1.5
0.1 Ë 0.5 Ë
Ë Ë
○ −
AnythingTest BuildNetwork Chord ClassicDeadlock ClassicPhil DanglingThreads DeadlockTwo GuardedLocks MayNotHappenInParallel NetworkAllP PhilTableP SimpleWhile StaticFields SynchMethod
36 52 37 48 51 59 34 30 26 52 60 31 28 21
2 3 1 1 2 1 1 1 1 3 4 2 1 1
5 4 7 6 8 10 5 3 3 4 5 3 3 3
77 112 67 73 217 91 112 64 53 112 203 80 65 46
172.4 157.1 306.8 148.4 148.6 150.4 149.8 165.3 166.1 147.8 331.1 155.0 167.1 169.3
0.4 0.5 2.5 0.4 0.6 0.5 0.5 0.5 0.4 0.4 3.7 0.4 0.5 0.5
0.2 0.1 0.9 0.1 0.2 0.1 0.1 0.1 0.2 0.1 0.8 0.1 0.1 0.1
Ë Ë Ë Ë Ë Ë Ë Ë Ë Ë Ë Ë Ë Ë
Ë Ë Ë Ë
Ë Ë
Ë − Ë Ë Ë Ë − + Ë − − Ë − Ë
40 25
4 2
3 3
72 51
148.7 148.5
0.4 0.3
0.1 Ë 0.1 Ë
Ë Ë
− Ë
42 59 55 57 59 45 50
1 2 4 6 4 3 3
5 9 7 7 7 4 6
73 234 71 71 91 12 73
322.4 162.0 314.9 313.4 314.5 303.4 317.0
2.9 0.8 88.9 214.5 3.2 0.9 2.9 0.7 4.1 1.0 2.1 0.5 2.8 0.7
Ë
Ë
Ë Ë Ë Ë Ë
○ ○ ○ ○ ○
Ë Ë ○ ○ ○ ○ ○
Chordv2 DeeperContextDeadlock DiningPhilP8T InnerThreads Interleaving JoinUnderLock Nested200T2 RecJoin RecUnbounded RecursiveJoinUnderLock WhileCnt2N2T
37 65 60 32 155 22 1015 44 69 35 34
1 1 3 1 1 1 1 1 3 1 1
47 7 8 186 19 666 54 4 30 547 3 40 6 1870 6 175 6 274 5 89 5 91
306.3 303.8 276.6 308.8 169.1 307.7 271.0 284.9 297.6 298.4 282.0
2.8 4.1 4.9 2.4 1.1 2.4 11.8 2.8 3.4 2.9 3.1
0.7 0.7 0.9 0.5 0.3 0.7 4.1 0.7 0.7 0.7 0.6
Ë Ë Ë Ë Ë Ë Ë Ë Ë Ë Ë
Chord ClassicDeadlock When
41 29 45
1 1 1
6 2 4
148.3 147.9 148.4
0.5 0.5 0.5
0.1 Ë 0.1 Ë 0.1 Ë
2738 70
76 2
✓ ✓
Deadlock1 Deadlock2 ClassicDeadlockN PhilTable Records Sealedclasses Switch VirtualThreads Yield
✓
88 64 89
Ë Ë Ë Ë Ë
Ë Ë Ë Ë Ë Ë Ë Ë Ë Ë
− − − Ë − − − − − ○ ○ ○
238 6624 8818.8 164.2 234.2 6 170 226.1 4.2 6.0
Table 2: Experimental subjects and results. For each group of programs used to evaluate jPetrify, the table lists the name of each program in the group, whether the program is correct ✓ has a deadlock , its size in lines of code loc, number of classes and methods. The table also reports the size |PN| in number of places of jPetrify’s PN model of the program, the times (in seconds) for soot’s analysis, jPetrify’s PN encoding, and LoLA’s verification. The right-hand side details the outcome of verification with each tool: jPetrify, JPF, and JaDA: success Ë, false negative −, false positive +, time out/out of memory , and failure due to unsupported features ○.
unnecessarily large number of lock-thread combinations, which results in a huge state space on which jPetrify runs out of memory. This example showcases a current limitation of jPetrify, which depends on the precision of Soot’s alias analysis. The flip side is that plugging in a bespoke alias analysis—something for future work—in jPetrify’s implementation will improve its precision without changes to the underlying technique. Language feature support. Since jPetrify targets bytecode, it can verify programs in group variants that use features that have only been available in recent Java versions. In contrast, both JPF and JaDA fail to analyze 5 examples in variants since they do not support recent language features; for the same reason, JaDA also fails on the BankTransfer example that uses lambdas. jPetrify can also analyze the 3 examples written in Kotlin; somewhat 15
surprisingly, JPF could also analyze them, since the tool can be configured to directly input bytecode. Instead, JaDA works only on source code, and hence it is limited to programs written in Java. As explained above, we deliberately selected these examples to demonstrate jPetrify’s adaptability to recent Java features and other JVM languages; jPetrify has other language limitations, which we discussed in Sec. 5. Scalability. jPetrify successfully analyzed 4 examples in group size and 3 examples in group JaDA on which JPF ran out of memory. This indicate that JPF struggles to scale to programs with significant usage of recursion (ClassicPhil, DiningPhilP8T, Chordv2, PhilTableP) or a large number of interleavings (SimpleWhile, WhileCnt2N2T , Interleaving). Interestingly, JPF times out too on the one example PhilTable where jPetrify runs out of memory. While JaDA’s abstractions make it a generally more scalable tool, it still timed out on 2 examples in group size that jPetrify can analyze. In all, these examples indicate that the kinds of complex behaviors that jPetrify can analyze are somewhat complementary to the focus of tools based on different approaches. Soundness and precision. In all our experiments neither jPetrify nor JPF produced any false positives or false negatives. While Petrify relies on approximations, which we presented formally in the paper, that may break soundness or precision, these experiments indicate that jPetrify remains practically applicable on numerous examples despite its theoretical limitations. In contrast, JaDA incurred 15 false negatives and 1 false positive in the experiments. The false negatives indicate that its abstractions are not sound in general, since they sometimes omit program interactions that are feasible and may trigger a deadlock. The false positive (GuardedLocks) is simply a result of an imprecise overapproximation of the possible sequential executions under locking. Evaluation summary. Our evaluation indicates that jPetrify is applicable to programs using modern Java features, including concurrency features such as virtual threads. Despite being a prototype, jPetrify can tackle programs with complex control flow (nested conditionals, loops, recursion) and dynamic, unbounded thread creation. Its main limitations are the lack of support for Java features like exceptions and arrays, and its imprecision in the presence of complex aliasing. Overall, its current capabilities and limitations complement other Java concurrency analysis tools. Limitations. Our experiments are are not meant to be a direct comparison between jPetrify and JPF and JaDA, both because JaDA and, especially, JPF are much more mature tools, and because their characteristics are largely complementary.
7
Conclusions
This paper presented Petrify: a technique to analyze concurrency properties of Java programs based on model-checking an encoding of a flow- and context-sensitive, pathinsensitive approximation of the bytecode semantics. Two characteristics distinguish Petrify’s approach from other automated verification techniques for concurrent Java: i) Petrify uses Petri nets (PNs) to approximate the program’s concurrent behavior and to apply model checking. ii) Petrify operates on Java bytecode rather than source code. This brings several practical advantages, in particular in terms of robustness and flexibility. The experiments we discussed in the paper demonstrate the practical advantages brought by Petrify’s design choice, as well as its current limitations. Even though jPetrify is still a prototype tool, we could find several examples of programs that challenge other more mature Java automated concurrency verification tools that it can analyze successfully. 16
References 1. Blackshear, S., Gorogiannis, N., O’Hearn, P.W., Sergey, I.: RacerD: compositional static race detection. Proc. ACM Program. Lang. 2(OOPSLA), 144:1–144:28 (2018) 2. Blom, S., Darabi, S., Huisman, M., Oortwijn, W.: The VerCors tool set: Verification of parallel and concurrent software. In: Integrated Formal Methods – 13th International Conference (IFM) 2017, Turin, Italy, September 20–22, 2017, Proceedings. Lecture Notes in Computer Science, vol. 10510, pp. 102–110. Springer (2017) 3. Bourdil, P.A., Berthomieu, B., Dal Zilio, S., Vernadat, F.: Symmetry reduction for time Petri net state classes. Science of Computer Programming 132 (09 2016). https://doi.org/10.1 016/j.scico.2016.08.008
4. de Carvalho Gomes, P., Gurov, D., Huisman, M., Artho, C.: Specification and verification of synchronization with condition variables. Sci. Comput. Program. 163, 174–189 (2018) 5. Cordeiro, L.C., Kesseli, P., Kroening, D., Schrammel, P., Trtík, M.: JBMC: A bounded model checking tool for verifying java bytecode. In: Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, Part I. Lecture Notes in Computer Science, vol. 10981, pp. 183–190. Springer (2018) 6. Distefano, D., Fähndrich, M., Logozzo, F., O’Hearn, P.W.: Scaling static analyses at Facebook. Commun. ACM 62(8), 62–70 (2019) 7. Farzan, A., Madhusudan, P.: Causal atomicity. In: Computer Aided Verification, 18th International Conference, CAV 2006, Seattle, WA, USA, August 17-20, 2006, Proceedings. Lecture Notes in Computer Science, vol. 4144, pp. 315–328. Springer (2006) 8. Ferrara, P.: A generic static analyzer for multithreaded Java programs. Softw. Pract. Exp. 43(6), 663–684 (2013) 9. Furia, C.A., Mandrioli, D., Morzenti, A., Rossi, M.: Modeling Time in Computing. Monographs in Theoretical Computer Science. An EATCS series, Springer (2012) 10. Havelund, K., Pressburger, T.: Model checking Java programs using Java PathFinder. Int. J. Softw. Tools Technol. Transf. 2(4), 366–381 (2000) 11. Jacobs, B., Smans, J., Philippaerts, P., Vogels, F., Penninckx, W., Piessens, F.: VeriFast: A powerful, sound, predictable, fast verifier for C and Java. In: NASA Formal Methods - Third International Symposium, NFM 2011, Pasadena, CA, USA, April 18-20, 2011. Proceedings. Lecture Notes in Computer Science, vol. 6617, pp. 41–55. Springer (2011) 12. Java deadlocks examples. https://github.com/abelunibo/Java-Deadlocks (2025) 13. Jorshari, M.H.K., Kokologiannakis, M., Majumdar, R., Nagendra, S.: Optimal concolic dynamic partial order reduction. In: 36th International Conference on Concurrency Theory, CONCUR 2025, Aarhus, Denmark, August 26-29, 2025. LIPIcs, vol. 348, pp. 26:1–26:22. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2025) 14. Kahsai, T., Rümmer, P., Schäf, M.: JayHorn: A Java model checker (competition contribution). In: Tools and Algorithms for the Construction and Analysis of Systems - 25 Years of TACAS: TOOLympics, Held as Part of ETAPS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings, Part III. Lecture Notes in Computer Science, vol. 11429, pp. 214–218. Springer (2019) 15. Kester, D., Mwebesa, M., Bradbury, J.S.: How good is static analysis at finding concurrency bugs? In: Tenth IEEE International Working Conference on Source Code Analysis and Manipulation (SCAM) 2010, Timisoara, Romania, 12–13 September 2010. pp. 115–124. IEEE Computer Society (2010) 16. Kordon, F., Hulin-Hubard, F., Jezequel, L., Paviot-Adet, E., Nivon, Q., , Amat., N., Berthomieu, B., Dal Zilio, S., , Ding, Z., He, Y., Li, S., Jiang, C., Jensen, P., Srba, J., Thierry-Mieg, Y.: Complete Results for the 2025 Edition of the Model Checking Contest. https://mcc.lip6.fr/2025/results.php (June 2025)
17
17. Koval, N., Fedorov, A., Sokolova, M., Tsitelov, D., Alistarh, D.: Lincheck: A practical framework for testing concurrent data structures on JVM. In: Computer Aided Verification 35th International Conference, CAV 2023, Paris, France, July 17–22, 2023, Proceedings, Part I. Lecture Notes in Computer Science, vol. 13964, pp. 156–169. Springer (2023) 18. Kulkarni, R., Mathur, U., Pavlogiannis, A.: Dynamic data-race detection through the finegrained lens. In: 32nd International Conference on Concurrency Theory, CONCUR 2021, Virtual Conference, August 24-27, 2021. LIPIcs, vol. 203, pp. 16:1–16:23. Schloss Dagstuhl Leibniz-Zentrum für Informatik (2021) 19. Laneve, C., Garcia, A.: Deadlock detection of Java bytecode. In: Logic-Based Program Synthesis and Transformation - 27th International Symposium, LOPSTR 2017, Namur, Belgium, October 10-12, 2017, Revised Selected Papers. Lecture Notes in Computer Science, vol. 10855, pp. 37–53. Springer (2017) 20. Leavens, G.T.: Tutorial on JML, the Java modeling language. In: 22nd IEEE/ACM International Conference on Automated Software Engineering (ASE 2007), November 5-9, 2007, Atlanta, Georgia, USA. p. 573. ACM (2007) 21. Lee, Z.H., Mathur, U.: Efficient decrease-and-conquer linearizability monitoring. Proc. ACM Program. Lang. 9(OOPSLA2) (Oct 2025). https://doi.org/10.1145/3763123, https://doi.org/10.1145/3763123
22. Lin, Z., Marinov, D., Zhong, H., Chen, Y., Zhao, J.: JaConTeBe: A benchmark suite of real-world Java concurrency bugs (T). In: 30th IEEE/ACM International Conference on Automated Software Engineering, ASE 2015, Lincoln, NE, USA, November 9–13, 2015. pp. 178–189. IEEE Computer Society (2015) 23. Livshits, B., Sridharan, M., Smaragdakis, Y., Lhoták, O., Amaral, J.N., Chang, B.E., Guyer, S.Z., Khedker, U.P., Møller, A., Vardoulakis, D.: In defense of soundiness: a manifesto. Commun. ACM 58(2), 44–46 (2015) 24. Ma, X., Wu, S., Pobee, E.B., Mei, X., Zhang, H., Jiang, B., Chan, W.K.: Regiontrack: A trace-based sound and complete checker to debug transactional atomicity violations and non-serializable traces. ACM Trans. Softw. Eng. Methodol. 30(1), 7:1–7:49 (2021) 25. Mathur, U., Viswanathan, M.: Atomicity checking in linear time using vector clocks. In: ASPLOS ’20: Architectural Support for Programming Languages and Operating Systems, Lausanne, Switzerland, March 16-20, 2020. pp. 183–199. ACM (2020) 26. Müller, P., Schwerhoff, M., Summers, A.J.: Viper: A verification infrastructure for permissionbased reasoning. In: Verification, Model Checking, and Abstract Interpretation - 17th International Conference, VMCAI 2016, St. Petersburg, FL, USA, January 17-19, 2016. Proceedings. Lecture Notes in Computer Science, vol. 9583, pp. 41–62. Springer (2016) 27. Shenoy, A., Furia, C.A.: jPetrify: implementation and experiments. https://figshare.com /s/a52661ae052b64808d0e (May 2026) 28. Thokair, M.A., Zhang, M., Mathur, U., Viswanathan, M.: Dynamic race detection with O(1) samples. Proc. ACM Program. Lang. 7(POPL), 1308–1337 (2023) 29. Tunç, H.C., Mathur, U., Pavlogiannis, A., Viswanathan, M.: Sound dynamic deadlock prediction in linear time. Proc. ACM Program. Lang. 7(PLDI), 1733–1758 (2023) 30. Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification. In: Proceedings of the Symposium on Logic in Computer Science (LICS ’86), Cambridge, Massachusetts, USA, June 16-18, 1986. pp. 332–344. IEEE Computer Society (1986) 31. Wolf, K.: Petri net model checking with LoLA 2. In: Application and Theory of Petri Nets and Concurrency - 39th International Conference, PETRI NETS 2018, Bratislava, Slovakia, June 24-29, 2018, Proceedings. Lecture Notes in Computer Science, vol. 10877, pp. 351–362. Springer (2018)
18
A
Additional details for Sec. 5.1
Conditionals: Translating conditionals with nondeterministic jumps is sound but pathinsensitive; hence, it generally involves a loss of precision, because 𝑅 may include paths that are unfeasible in 𝐽 due to unsatisfiable path conditions. For example, the error location is unreachable in Fig. 6a’s Jimple program (left) because the condition of the if is identically false; however, it becomes reachable in the rb translation (right) where the condition is abstracted away. Reentrant locks: The translation of lock operations in 𝐽 with acquire and release in 𝑅 is sound provided the lock is not used reentrantly. According to Fig. 3, rb does not allow a thread to acquire a lock on 𝑘 if it already holds a lock on it; thus, 𝑅 may omit such executions even if they are possible in 𝐽.4 For example, if lock is a reentrant lock variable, the error location is reachable in Fig. 6b’s Jimple program (left), where the same thread acquires lock twice in a row; in contrast, the second acquire of lock in the corresponding rb program (right) never executes (since Fig. 3’s semantics does not allow it), and hence error becomes effectively unreachable. Calls: Petrify’s sound translation of call instructions depends on the capabilities of Soot’s analysis. In particular, invokedynamic instructions are correctly translated only if Soot can retrieve the body of the invoked closure object. This is possible in simple cases such as Fig. 1’s example, where invokedynamic is used to execute the Runnable lambdas lock_12 and lock_21; more complex instances of invokedynamic would become skip in 𝑅, which introduces unsoundness in general. For example, consider an invoke dl, where dl resolves to a method that causes a deadlock when executed; if Soot cannot resolve dl statically, the call becomes simply skip in rb, and hence Petrify would unsoundly conclude that there is no deadlock. Unsupported instructions: Other bytecode instructions that are not listed in Fig. 2a are currently unsupported by Petrify. The translation replaces any unsupported instruction 𝐼 with a skip, which means that 𝑅 doesn’t model 𝐼’s semantics. This may result in a loss of soundness or precision, depending on what execution paths the unsupported instruction does enable or block. For example, consider the Jimple code in Fig. 6c (left): the throw instruction unconditionally jumps to location ℓ2 , where a matching catch block is defined; therefore, location ℓ1 is unreachable in the original program, since it is just after the throw. Since Petrify does not currently support exception-related instructions such as throw, this instruction becomes simply a skip in the rb translation (right); thus, ℓ1 is reachable in the rb program, whereas ℓ2 is unreachable. As a result of this translation, analyzing the rb program in lieu of the Jimple program may be unsound (if the code at ℓ2 introduces an error, which would go undetected in the rb program), imprecise (if the unreachable code at ℓ1 introduces an error, which would be spuriously detected in the rb program), or possibly neither (if the code at ℓ1 and ℓ2 do not affect program correctness w.r.t. the properties Petrify analyzes). Aliasing: Two variables 𝑣 1 , 𝑣 2 that may be aliased in 𝐽 are lumped together into a single variable 𝑣 = 𝛼(𝑣 1 ) = 𝛼(𝑣 2 ) in 𝑅; this may introduce a loss of soundness or, more 4 Soundly modeling reentrant locks would require a stack-like counting mechanism, which goes
beyond the expressiveness of plain PNs; hence, it belongs to future work.
19
commonly, precision. Fig. 6d shows an example where imprecise aliasing information introduces unsoundness: the two threads t_1 and t_2 acquire lock_1 and lock_2 in opposite order, which clearly may result in a deadlock. If the alias analysis erroneously determines that the two lock variables may be aliased, Petrify models them as a single variable lock; thus, in the rb encoding, a deadlock cannot occur because both threads try to acquire the same lock twice in a row (a case of reentrant locking, which is ignored by rb’s semantics as we discussed above). Fig. 6e shows an example where imprecise aliasing information introduces imprecision: thread t_1 acquires lock_1 and then lock_2, whereas thread t_2 acquires lock_2 and then lock_3. If these are all distinct locks, no deadlock can occur. However, if the alias analysis erroneously determines that lock variables lock_1 and lock_3 may be aliased, Petrify models them as a single variable lock_13; thus, in the rb encoding, a deadlock may occur because both threads are in contention to acquire lock_13 and lock_2 in opposite order.
B
Additional details for Sec. 5.2
The PN encoding of commands in Fig. 5 is as follows: a) Commands skip, read, and write transfer the token from place ( 𝑝, 𝑡, ℓ, 𝑟) to the next location’s place ( 𝑝, 𝑡, ℓ + 1, 𝑟). b) Command goto ℓ ′ transfers the token from the place ( 𝑝, 𝑡, ℓ, 𝑟) to the unconditional jump’s target’s place ( 𝑝, 𝑡, ℓ ′ , 𝑟). c) Similarly, command jump ℓ1 ℓ2 nondeterministically transfers the token to either place ( 𝑝, 𝑡, ℓ1 , 𝑟) or place ( 𝑝, 𝑡, ℓ2 , 𝑟). d) Command fork 𝑝 ′ 𝑡 ′ puts one token into the next location’s place, and one token into the forked thread’s entry point’s place ( 𝑝 ′ , 𝑡 ′ , entry 𝑝′ , 𝑟). This way, the forked thread’s computation can proceed in parallel to the forking thread’s. e) Conversely, join 𝑡 ′ can fire only when the exit transition ( 𝑝 ′ , 𝑡 ′ , exit 𝑝′ , 𝑟) of thread 𝑡 ′ fires (where 𝑝 ′ is the procedure that thread 𝑡 ′ is running). f ) Command acquire 𝑣’s transition can fire only if all places (𝑡 ′ , 𝑣) are marked, denoting that no thread 𝑡 ′ holds a lock on 𝑣. When it fires, it puts back a token only in place (𝑡, 𝑣) to indicate that 𝑡 holds a lock on 𝑣. g) Command release 𝑣’s transition can fire only if place (𝑡, 𝑣) is marked, denoting that thread 𝑡 holds a lock on 𝑣. When it fires, it puts back a token in all places (𝑡 ′ , 𝑣), thus allowing other threads to acquire a lock on 𝑣. h) When the transition ( 𝑝, 𝑡, ℓ, 𝑟) of command call 𝑝 ′ fires, it puts a token in the callee’s entry place ( 𝑝 ′ , 𝑡, entry 𝑝′ , ℓ). Then, execution continues in the subnet corresponding procedure 𝑝 ′ called in thread 𝑡 at call site ℓ. Then, when transition ( 𝑝 ′ , 𝑡, exit 𝑝′ , ℓ) fires, signaling that the subnet’s execution has terminated, a token first goes into return place ( 𝑝 ′ , 𝑡, ↩→ ℓ); then one of the transitions ( 𝑝, 𝑡, ↩→ ℓ, 𝑟), for all possible callers of 𝑝 ′ , nondeterministically fires. Fig. 5h pictures two callers 𝑟 1 ≠ 𝑟 2 , where either of the return transitions ( 𝑝, 𝑡, ↩→ ℓ, 𝑟 𝑘 ), 𝑘 = 1, 2, may fire when the subnet terminates execution. This nondeterministic encoding of returns is the only aspect of Petrify’s encoding 20
if false error
jump ℓ error ℓ: goto ok error: . . . ok: . . .
goto ok error: ok:
... ...
(a) A conditional in bytecode (left) whose rb translation (right) is imprecise.
monitor_enter lock monitor_enter lock error:
acquire lock acquire lock error: // unreachable
...
(b) A lock used reentrantly in bytecode (left) whose rb translation (right) is unsound.
throw e
skip
ℓ1 : . . .
ℓ1 : . . .
// catch(e) block
// catch(e) block
ℓ2 : . . .
ℓ2 : . . .
(c) Translating an unsupported bytecode instruction such as throw (left) to skip in rb (right) may introduce unsoundness (if ℓ2 is an error location, unreachable in rb but reachable in Jimple) or imprecision (if ℓ1 is an error location, reachable in rb but unreachable in Jimple).
// thread t_1 monitor_enter lock_1 monitor_enter lock_2
acquire lock
// thread t_1
// thread t_2 monitor_enter lock_2 monitor_enter lock_1
acquire lock
acquire lock // thread t_2 acquire lock
(d) If the alias analysis of the bytecode program on the left indicates that lock_1 and lock_2 may be aliases even though they are actually not, the rb translation (right) would render them as a single lock variable. This is unsound because the rb program would not deadlock even if the bytecode program it translates may deadlock.
// thread t_1 monitor_enter lock_1 monitor_enter lock_2
acquire lock_13 acquire lock_2
// thread t_1
// thread t_2 monitor_enter lock_2 monitor_enter lock_3
acquire lock_2 acquire lock_13
// thread t_2
(e) If the alias analysis of the bytecode program on the left indicates that lock_1 and lock_3 may be aliases even though they are actually not, the rb translation (right) would render them as a single lock_13 variable. This is imprecise because the rb program may deadlock even if the bytecode program it translates obviously does not deadlock.
Fig. 6: Examples of Jimple programs whose rb translation by Petrify may be unsound or imprecise.
of rb programs that loses precision: a PN cannot store an unbounded stack of return locations,5 and hence Petrify overapproximates it with a nondeterministic choice. 5 PNs with inhibitor arcs would be able to simulate this without loss of precision; however, their
reachability problem becomes undecidable [9].
21
monitor 𝜙𝑇 termination
ctl temporal logic formula AF D ∧ ∀𝑝 : 𝑃, 𝑡 : 𝑇, 𝑟 : 𝐿, 𝜏 : {○,
𝑝𝑡 𝑝𝑡𝑟
} · 𝑚( 𝑝, 𝑡, 𝑟, 𝜏) = 0
𝑝𝑡𝑟 entry 𝑟 ○
𝑝𝑡 𝑝𝑡𝑟
𝜙 𝐷 deadlock 𝜙 𝐿 livelock
é
exit 𝑟
EF EG D ∧ ∃𝑝 : 𝑃, 𝑡 : 𝑇, 𝑟 : 𝐿, 𝜏 : {○, } · 𝑚( 𝑝, 𝑡, 𝑟, 𝜏) ≠ 0 EF EG ¬D ∧ ∃𝑝 : 𝑃, 𝑡 : 𝑇, 𝑟 : 𝐿, 𝜏 : {○, } · 𝑚( 𝑝, 𝑡, 𝑟, 𝜏) ≠ 0
Table 3: How Petrify checks for various concurrency properties.
Proof (Proof outline of Lemma 1). Let 𝑆0 ⇝ 𝑆1 ⇝ · · · be a sequence of states in 𝑃’s semantics. Each 𝑆 𝑘 maps to a marking 𝑚 𝑘 of 𝑁 as follows. For every (𝑡, 𝑝, ℓ, 𝐾, 𝑅, 𝜏) ∈ 𝑆 𝑘 , let 𝜌 = ⊤ if 𝑅 = ∅, and 𝜌 = 𝑟 if 𝑅 = 𝑅 ′ + [𝑟 + 1]. Then, the following places are marked in 𝑁: i) ( 𝑝, 𝑡, ℓ, 𝜌) if 𝜏 = ; ii) ( 𝑝, 𝑡, ⊲⊳ ℓ, 𝜌) if 𝜏 = é; iii) (𝑡, 𝑘) for every 𝑘 ∈ 𝐾. Furthermore, for every 𝑘 ′ such that 𝑘 ′ ∉ 𝐾 ′ for every tuple (𝑡 ′ , 𝑝 ′ , ℓ ′ , 𝐾 ′ , 𝑅 ′ , 𝜏) ∈ 𝑆, all places (𝑡 ′ , 𝑘 ′ ) are also marked. In particular, this mapping translates 𝑃’s initial state {(𝑡0 , main, entrymain , ∅, ∅, )} into 𝑁’s initial marking. Then, one can show by induction that if 𝑆 𝑘 ⇝ 𝑆 𝑘+1 then 𝑚 𝑘 ⊢1,2 𝑚 𝑘+1 , where 1,2 ⊢ denotes one or two steps in 𝑁’s semantics. Precisely, the only scenario when a step in 𝑃’s evaluation corresponds to two consecutive markings in 𝑁’s semantics is when 𝑠 = (𝑡, 𝑝, exit 𝑝 , 𝐿, 𝑅 + [ℓ], ) ∈ 𝑆 𝑘 ⇝ 𝑆 𝑘 \ {𝑠} ∪ {(𝑡, 𝑝 ′ , ℓ, 𝐿, 𝑅, )}; in this case, 𝑚 𝑘 ⊢ 𝑚 ′𝑘 ⊢ 𝑚 𝑘+1 where 𝑚 ′𝑘 is the marking reached after transition ( 𝑝, 𝑡, exit 𝑝 , ℓ) fires, moving a token from place ( 𝑝, 𝑡, exit 𝑝 , ℓ) to ( 𝑝, 𝑡, ↩→ ℓ), and 𝑚 𝑘+1 corresponds to the nondeterministically chosen return location (as shown in Fig. 5h).
C
Additional details for Sec. 5.3
Petrify takes care of expressing these properties for the PN analyzer, so that the user
does not have to directly interact with the latter. For this work, we focus on three widely useful concurrency properties: termination, deadlock, and livelock. In future work, we will extend this approach to support other concurrency properties, such as data races and atomicity—even though one can already analyze these properties by directly expressing them in the language of the PN analyzer. In order to analyze a property 𝜙 on a PN 𝑁, Petrify first extends 𝑁 with additional places and transitions that act as monitors of 𝑁’s state components that are useful to check for the properties. While using monitors is not strictly needed, it helps simplify the temporal logic formula that expresses the properties, which in turn results in performance benefits. Tab. 3 shows the monitors and temporal logic formulas built by Petrify to verify properties termination 𝜙𝑇 (which holds if the program always terminates), deadlock 𝜙 𝐷 (which holds if the program may deadlock) and livelock 𝜙 𝐿 (which holds if the program may livelock). These three properties use the same monitor: for each subnet corresponding to thread 𝑡 executing procedure 𝑝 with return location 𝑟, the monitor adds two places ( 𝑝, 𝑡, 𝑟, ○) and ( 𝑝, 𝑡, 𝑟, ), and a transition ( 𝑝, 𝑡, 𝑟, é). As soon as a subnet’s entry (resp. exit) transition fires, place ( 𝑝, 𝑡, 𝑟, ○) (resp. ( 𝑝, 𝑡, 𝑟, )) gets a token; when both places are marked, transition ( 𝑝, 𝑡, 𝑟, é) fires and empties them. Therefore, ( 𝑝, 𝑡, 𝑟, ○) is marked iff the subnet is executing. 22
With this monitor, Tab. 3’s CTL formulas express the three properties of termination, deadlock, and livelock. The formulas use predicate D, which is built-in most PN analyzers and denotes a PN deadlock: a situation where all transitions in the PN are permanently disabled. In Petrify’s encoding 𝑁, a PN deadlock does not necessarily correspond to a deadlock of program 𝐽: if all threads have completed execution normally (or have never been started), a PN deadlock simply denotes normal termination; but if some threads have not completed execution, a PN deadlock corresponds to a program deadlock. Petrify correctly distinguishes between deadlocks and termination also in cases where some threads are forked but not joined by expressing properties on the monitor’s places as follows: i) Termination: the program eventually terminates iff all the threads that have started eventually finish execution. Thus, 𝜙𝑇 checks that, along all execution paths in the future (CTL operator AF), the PN deadlocks (predicate D, which indicates that no transition can fire) and all ○ and places are empty (which indicates that no thread is executing). ii) Deadlock: the program is stuck and cannot reach proper termination or make progress. Thus, 𝜙 𝐷 checks that, along all execution paths from some point on in the future (CTL operator EF EG), the PN deadlocks (predicate D, which indicates that no transition can fire) and at least one ○ and place remains not empty (which indicates that some thread has started but cannot complete execution). The non-empty places correspond to the deadlocked threads. iii) Livelock: the program as a whole can continue execution, but one or more threads cannot terminate or make progress. Thus, 𝜙 𝐿 checks that, along all execution path from some point on in the future (CTL operator EF EG), the PN does not deadlock (¬D, since the program as a whole still runs) but at least one ○ and place remains not empty indefinitely (which indicates that some thread has started but cannot complete execution). The non-empty places correspond to the threads that can’t reach termination. Example 6. Fig. 1c’s parts in purple monitor the termination of each thread as in Tab. 3. Since the main thread does not join the two spawned threads, this is a situation where a deadlock of the PN (i.e., EF EG (D) holds) does not imply a deadlock of the original program. This is where Petrify’s monitor is used to distinguish the two scenarios: if all procedures terminate normally, Tab. 3’s formula 𝜙 𝐷 will never hold, since all ○, places will eventually be empty. In contrast, when the PN reaches the state where the light red places are marked, places ( t_12, ○) and ( t_21, ○) will remain marked too; thus, the state exposes a genuine deadlock in Fig. 1a’s original program, which satisfies formula 𝜙 𝐷 . ■ C.1
Implementation Details and Limitations
We implemented the Petrify technique in a command-line tool called jPetrify. jPetrify inputs a bytecode program 𝐽, uses Soot to analyze Jimple code and its control-flow, and produces a PN 𝑃 = E (T (𝐽)) as described in previous sections. As we discussed previously in this section, Petrify’s output 𝑃 is a sound model of the execution order of instructions in 𝐽 provided the following conditions are met: 23
i) Soot’s alias analysis of lock variables in 𝐽 is sufficiently accurate (as explained in Sec. 5.1); ii) 𝐽 does not use unsupported bytecode features (mainly, exceptions and invokedynamic calls that Soot cannot resolve); iii) 𝐽 does not use any lock reentrantly (i.e., a thread acquires a lock on a variable it’s already locking). Under these conditions, if a temporal logic property 𝜙 holds on 𝑃, then it also holds on 𝐽. Conversely, Petrify’s output 𝑃’s precision as a model of 𝐽’s executions depends on several factors: i) The accuracy of the points-to alias analysis also affects precision. Currently, jPetrify uses Soot’s Spark whole-program analysis, which induces a significant loss of precision with features such as array indexing. ii) Path-sensitive information is ignored in 𝑃, which means that all control-flow paths in 𝐽 are feasible in 𝑃. iii) Context-sensitive information is overapproximated by 𝑃, so a call may nondeterministically return to any of its possible call sites in 𝐽. iv) Finally, below we outline how Petrify’s modeling of loops and recursion affects its precision. The experiments in Sec. 6 assess the practical impact of Petrify’s current limitations. void main() { do { Thread t = new Thread(() -> { 𝑝 }); t.start(); if (. . .) t.join(); } while (. . .); }
def main entrymain : begin ℓ0 : fork 𝑝 t ℓ1 : jump ℓ2 ℓ3 ℓ2 : join t ℓ3 : jump ℓ0 , exitmain exitmain : end
m 𝑡0 m 𝑡0
ℓ3 → ℓ0
m 𝑡0
m 𝑡0
m 𝑡0
m 𝑡0
m 𝑡0
ℓ1 → ℓ3 m 𝑡0
m 𝑡0
m 𝑡0
m 𝑡0
entrym
entrym
ℓ0
ℓ0
ℓ1
ℓ1 → ℓ2
ℓ2
ℓ2 m 𝑡0
ℓ3
𝑝t
m 𝑡0
m 𝑡0
ℓ3 → exitm exitm
exitm
𝑝t ⊲⊳ ℓ2
··· entry 𝑝
m 𝑡0
exit 𝑝
Fig. 7: Petri net encoding of an rb program that models a Java program that spawns threads in a loop. For readability, procedure main is abbreviated as m in the Petri net.
Threads and Loops. Fig. 7 demonstrates how unbounded loops are handled by Petrify, and how they affect precision. The Java program shown there starts a certain number of threads in a loop and joins some of them. As long as the code 𝑝 executed by the spawned threads does not introduce a circular wait dependency with the main thread, the program does not deadlock. Let us see how this behavior is captured accurately by the rb model, and in turn by the PN encoding, shown in the same figure. 24
def main entrymain : begin ℓ0 : call rec ℓ1 : release lock exitmain : end
var lock = new Lock(); static void main() { rec(); lock.unlock(); }
def rec entryrec : begin 𝑟0 : acquire lock 𝑟1 : jump 𝑟2 exitrec 𝑟2 : release lock 𝑟3 : call rec exitrec : end
static void rec() { lock.lock(); if (. . .) { lock.unlock(); rec(); } }
m
m
m
m
enm ⊤
enm ⊤
ℓ0 ⊤
ℓ0 ⊤
m
m
m
m
exm ⊤
exm ⊤
ℓ1 ⊤
ℓ1 ⊤
r
r
r
r
r
r
r
𝑟2 ℓ0
𝑟3 ℓ0
𝑟3 ℓ0
exr ℓ0
exr ℓ0
𝑟1→𝑟2 ℓ0 𝑟2 ℓ0 r
r
r
r
enr ℓ0
enr ℓ0
𝑟0 ℓ0
𝑟0 ℓ0
r
r
r
𝑟3 𝑟3
𝑟3 𝑟3
𝑟2 𝑟3
r
r
r
r
↩→ ℓ0 ⊤ ↩→ ℓ0
r
r
↩→ 𝑟3 ℓ0
𝑟1 ℓ0 𝑟1→exr ℓ0
r
r
r
r
r
r
r
r
𝑟1 𝑟3
𝑟0 𝑟3
𝑟0 𝑟3
enr 𝑟3
enr 𝑟3
exr 𝑟3
exr 𝑟3
↩→ 𝑟3
r
𝑟2 𝑟3 𝑟1→𝑟2 𝑟3
r
r
𝑟1→exr 𝑟3
↩→ 𝑟3 𝑟3
Fig. 8: Petri net encoding of an rb program that models a Java program that recursively acquires and releases a lock. For readability, procedures main and rec are abbreviated as m and r in the Petri net; labels entry and exit are abbreviated as en and ex; and the places for lock variable lock are not shown explicitly, but the transitions corresponding to acquire and release are highlighted and
.
25
First, notice that the set 𝑇 of thread identifiers in the rb program is {𝑡0 , t}; in general, since threads are distinguished by their program identifiers up to aliasing, 𝑇 is always finite in an rb program. For each started thread, a new tuple ( 𝑝, t, entry 𝑝 , ∅, ∅, ) is added to the state 𝑆; correspondingly, a token is added to place ( 𝑝, t, entry 𝑝 ) in the PN, modeling the asynchronous execution of several threads. In general, the PN and the rb program have infinitely many executions, whereas the Java program will probably only execute the loop a finite number of times. Another source of overapproximation is the conditional in the loop body, which may be deterministic in the Java program but is nondeterministic in the rb and PN models. Nevertheless, the analysis of deadlock behavior is still precise on the PN model, since whether the Java program deadlocks does not depend on how many times the loop or conditional are executed. This example demonstrates how the counting capabilities of PNs are sufficient to capture recurring thread spawning patterns while retaining precision in the analysis of certain concurrency properties. Recursion. Fig. 8 demonstrates how recursion in handled in jPetrify. The Java program shown there starts executing a recursive method rec; with each recursive call, a lock is acquired before deciding whether to continue with another recursive call or return to the caller. The rb program in Fig. 8 has the same behavior as the Java program, except for the nondeterministic control flow; concretely, this means that the rb program has infinitely many possible executions, one for each possible maximum recursion depth 𝑛 ≥ 0. Fig. 8 also shows (with minor simplifications discussed in the caption) the PN encoding the rb program built by Petrify. The top row of nodes corresponds to the procedure main. The rest of the PN consists of two structurally isomorphic subnets, each encoding procedure rec; precisely, there is one subnet for each invocation site of rec: the subnet in the middle of the picture corresponds to call rec at ℓ0 , while the bottom subnet corresponds to call rec at 𝑟 3 . When execution in the latter subnet terminates—signaled by a token in place ( r, ↩→𝑟 3 )—the call nondeterministically returns to either of the two call sites. This nondeterminism overapproximates the behavior of the rb program (and thus the Java program) since it includes computations where 𝑛 > 0 nested recursive calls return abruptly to main. This may reduce precision, since the PN includes executions that are infeasible in the original program. As the experiments in Sec. 6 demonstrate, this limitation in principle does not always impact the practical capabilities of jPetrify: as long as the additional executions introduced by the overapproximation do not generate spurious violations of the concurrency properties of interest, the loss of precision is immaterial.
26