Figure 2.23. Concrete Syntax for High-level Thread or Function Body
|
Figure 2.23, “Concrete Syntax for High-level Thread or Function Body” presents the concrete syntax for high-level thread or function body. High-level body is designed for manual Bogor model construction, and it offers high-level control structure constructs found in most imperative programming languages such as Java. In addition, it features guarded command and atomic constructs to naturally model concurrent programs.
A high-level body consists of a sequence of statements. These sequence of statements are translated for their low-level equivalents before model checking. We now describe the statement constructs available in BIR, and we illustrate how they are translated to low-level via examples.
Abstract Syntax Tree.
The top Java AST class for statement is the Statement class.
Atomic statement is used to group transitions into one indivisible block. Another thread cannot interleave the execution of atomic statement until it (normally or exceptionally) terminates.
Examples.
- High-level example:
system AtomicExample { int x; int y; active thread MAIN() { atomic x := x + 1; y := y + 1; end } } - Translated code in low-level:
system AtomicExample { throwable record A extends ANY_THROWABLE {} int x; int y; active thread MAIN() { ANY_THROWABLE atomicCatch$Local; loc loc0: do { Atomic.beginAtomic(); } goto loc1; loc loc1: do { x := x + 1; } goto loc2; loc loc2: do { y := y + 1; } goto loc3; loc loc3: do { Atomic.endAtomic(); } goto loc4; loc loc4: do { } return; loc atomicCatch: do { Atomic.endAtomic(); throw atomicCatch$Local; } goto atomicCatch; catch ANY_THROWABLE atomicCatch$Local at loc1, loc2 goto atomicCatch; } extension Atomic for edu.ksu.cis.bogor.projects.bogor.ext.atomicity.AtomicModule { actiondef beginAtomic (); actiondef endAtomic (); } throwable record ANY_THROWABLE {} }
Abstract Syntax Tree. The Java AST class for atomic statement is the AtomicStatement class.
While statement in BIR is similar to while statement in most imperative programming language, i.e., it iteratively execute its body until its condition is no longer hold.
Examples.
- High-level example:
system WhileExample { active thread MAIN() { int i := 0; while i < 10 do i := i + 1; end } } - Translated code in low-level:
system WhileExample { active thread MAIN() { int i := 0; boolean temp$0; loc loc0: do { temp$0 := i < 10; } goto loc1; loc loc1: when temp$0 do { } goto loc2; when !(temp$0) do { } goto loc4; loc loc2: do { i := i + 1; } goto loc3; loc loc3: do { } goto loc0; loc loc4: do { } return; } }
Abstract Syntax Tree. The Java AST class for while statement is the WhileStatement class.
If statement in BIR is also similar to if statement in most imperative programming languages, i.e., it executes its first body whose condition holds.
Examples.
- High-level example:
system IfExample { int i := 0; active[3] thread MAIN() { atomic if i < 1 do i := i + 1; elseif i < 2 do i := i + 2; else do i := i + 3; end end } } - Translated code in low-level:
system IfExample { int i := 0; active [3] thread MAIN() { boolean temp$0; boolean temp$1; ANY_THROWABLE atomicCatch$Local; loc loc0: do { Atomic.beginAtomic(); } goto loc1; loc loc1: do { temp$0 := i < 1; } goto loc2; loc loc2: when temp$0 do { } goto loc3; when !(temp$0) do { } goto loc5; loc loc3: do { i := i + 1; } goto loc4; loc loc4: do { } goto loc10; loc loc5: do { temp$1 := i < 1; } goto loc6; loc loc6: when temp$1 do { } goto loc7; when !(temp$1) do { } goto loc9; loc loc7: do { i := i + 1; } goto loc8; loc loc8: do { } goto loc10; loc loc9: do { i := i + 3; } goto loc10; loc loc10: do { Atomic.endAtomic(); } goto loc11; loc loc11: do { } return; loc atomicCatch: do { Atomic.endAtomic(); throw atomicCatch$Local; } goto atomicCatch; catch ANY_THROWABLE atomicCatch$Local at loc1, loc2, loc3, loc4, loc5, loc6, loc7, loc8, loc9 goto atomicCatch; } extension Atomic for edu.ksu.cis.bogor.projects.bogor.ext.atomicity.AtomicModule { actiondef beginAtomic (); actiondef endAtomic (); } throwable record ANY_THROWABLE {} }
Abstract Syntax Tree. The Java AST class for if-statement is the IfStatement class.
Choose statement non-deterministically executes its bodies whose conditions hold. Bogor first evaluates all the conditions, and in a full-state-space exploration mode, it introduces branches in the state-space for each body whose condition evaluates to true. The else body is executed only when the other conditions evaluate to false. Note that the conditions and the first instructions of the bodies whose conditions hold are evaluated atomically.
Examples.
- High-level example:
system ChooseExample { int i := 0; active[3] thread MAIN() { atomic choose when <i < 1> do i := i + 1; when <i < 2> do i := i + 2; else do i := i + 3; end end } } - Translated code in low-level:
system ChooseExample { int i := 0; active [3] thread MAIN() { boolean temp$0; boolean temp$1; boolean temp$2; ANY_THROWABLE atomicCatch$Local; loc loc0: do { Atomic.beginAtomic(); } goto loc1; loc loc1: do invisible { temp$0 := i < 1; temp$1 := i < 2; temp$2 := !((temp$0 || temp$1)); } goto loc2; loc loc2: when temp$0 do invisible { } goto loc3; when temp$1 do invisible { } goto loc5; when temp$2 do invisible { } goto loc7; loc loc3: do { i := i + 1; } goto loc4; loc loc4: do { } goto loc9; loc loc5: do { i := i + 2; } goto loc6; loc loc6: do { } goto loc9; loc loc7: do { i := i + 3; } goto loc8; loc loc8: do { } goto loc9; loc loc9: do { Atomic.endAtomic(); } goto loc10; loc loc10: do { } return; loc atomicCatch: do { Atomic.endAtomic(); throw atomicCatch$Local; } goto atomicCatch; catch ANY_THROWABLE atomicCatch$Local at loc1, loc2, loc3, loc4, loc5, loc6, loc7, loc8 goto atomicCatch; } extension Atomic for edu.ksu.cis.bogor.projects.bogor.ext.atomicity.AtomicModule { actiondef beginAtomic (); actiondef endAtomic (); } throwable record ANY_THROWABLE {} }
Abstract Syntax Tree. The Java AST class for choose statement is the ChooseStatement class.
Try statement is used to handle raised exceptions similar to the try-catch statement in Java. For each of catch clauses, a throwable record type and a local variable identifier must be supplied that indicate the throwable type to be caught and stored to the variable. Note that, the local variable has to be declared in the beginning of the thread and function body. When an exception is raised in the try body, then the catch clauses are considered in the order of its declaration. If there is no catch clause that handles the raised exception, then the exception is transferred to the caller function, or if it is a thread, then it is considered an uncaught exception, i.e., an error in the model.
Examples.
- High-level example:
system TryExample { throwable record NPE { } record A { int x; } active thread MAIN() { A a; NPE npe; try assert a.x > 0; catch (NPE npe) a := null; end } } - Translated code in low-level:
system TryExample { throwable record NPE {} record A { int x; } active thread MAIN() { A a; NPE npe; int temp$0; loc loc0: do { temp$0 := a.x; } goto loc1; loc loc1: do { assert temp$0 > 0; } goto loc2; loc loc2: do { } goto loc5; loc loc3: do { a := null; } goto loc4; loc loc4: do { } goto loc5; loc loc5: do { } return; catch NPE npe at loc0, loc1, loc2 goto loc3; } }
Abstract Syntax Tree. The Java AST class for try statement is the TryStatement class.
Return statement is used to exit from function (i.e., return to the caller) and thread (i.e., the thread dies) similar to Java. If the function has a return type, then the return statement should have an expression whose type is compatible with the return type.
Examples.
- High-level example:
system ReturnExample { active thread MAIN() { assert fact(3) == 6; } function fact(int x) returns int { return x <= 1 ? 1 : x * fact(x - 1); } } - Translated code in low-level:
system ReturnExample { active thread MAIN() { int temp$0; loc loc0: temp$0 := invoke fact(3) goto loc1; loc loc1: do { assert temp$0 == 6; } goto loc2; loc loc2: do { } return; } function fact(int x) returns int { boolean temp$0; int temp$1; int temp$2; int temp$3; loc loc0: do { temp$0 := x <= 1; } goto loc1; loc loc1: when temp$0 do { } goto loc2; when !(temp$0) do { } goto loc3; loc loc2: do { temp$1 := 1; } goto loc6; loc loc3: do { temp$2 := x - 1; } goto loc4; loc loc4: temp$3 := invoke fact(temp$2) goto loc5; loc loc5: do { temp$1 := x * temp$3; } goto loc6; loc loc6: do { } return temp$1; } }
Abstract Syntax Tree. The Java AST class for return statement is the ReturnStatement class.
Action statement represents a BIR action at the high-level body.
Examples.
- High-level example:
system ActionExample { int x; active thread MAIN() { x := x + 1; } } - Translated code in low-level:
system ActionExample { int x; active thread MAIN() { int temp$0; loc loc0: do { temp$0 := x; } goto loc1; loc loc1: do { x := temp$0 + 1; } goto loc2; loc loc2: do { } return; } }
Abstract Syntax Tree. The Java AST class for action statement is the ActionStatement class.
Atomic action statement represents a BIR action that is executed atomically similar to the atomic statement. This syntax is introduced for convenience.
Examples.
- High-level example:
system AtomicActionExample { int x; active thread MAIN() { <x := x + 1;> } } - Translated code in low-level:
system AtomicActionExample { int x; active thread MAIN() { ANY_THROWABLE atomicCatch$Local; loc loc0: do { Atomic.beginAtomic(); } goto loc1; loc loc1: do { x := x + 1; } goto loc2; loc loc2: do { Atomic.endAtomic(); } goto loc3; loc loc3: do { } return; loc atomicCatch: do { Atomic.endAtomic(); throw atomicCatch$Local; } goto atomicCatch; catch ANY_THROWABLE atomicCatch$Local at loc1 goto atomicCatch; } extension Atomic for edu.ksu.cis.bogor.projects.bogor.ext.atomicity.AtomicModule { actiondef beginAtomic (); actiondef endAtomic (); } throwable record ANY_THROWABLE {} }
Skip statement allows one to move to the next control point.
Examples.
- High-level example:
system SkipExample { active thread MAIN() { skip; choose do skip; do skip; end } } - Translated code in low-level:
system SkipExample { active thread MAIN() { boolean temp$0; boolean temp$1; loc loc0: do invisible { temp$0 := true; temp$1 := true; } goto loc1; loc loc1: when temp$0 do invisible { } goto loc2; when temp$1 do invisible { } goto loc3; loc loc2: do { } goto loc4; loc loc3: do { } goto loc4; loc loc4: do { } return; } }
Abstract Syntax Tree. The Java AST class for atomic action statement is the AtomicActionStatement class.