Large Block Encoding for Concurrent Programs

Large Block Encoding for Concurrent Programs

Tasks

11. Use the developer GUI to analyze a program.

Examples in trunk/examples/concurrent/

Toolchain trunk/examples/toolchains/PetriAutomizerBplInline.xml or trunk/examples/toolchains/PetriAutomizerCInline.xml

12. Write Boogie programs

Write two new concurrent Boogie program (one safe/one unsafe) that are related to your thesis.

13. Get familiar with AutomataScript and Petri nets

https://ultimate.informatik.uni-freiburg.de/?ui=int&tool=automata_library&task=automataScript&sample=151597609 Write two Petri nets that are related to your thesis. Demonstate somehow that large block encoding is speeding up automata operations

14. SV-COMP benchmarks

Get the pthread benchmarks from the SV-COMP https://sv-comp.sosy-lab.org/2019/ and verify one of these.

21. Inputs and Outputs of the algorithm

What are the inputs and outputs of the algorithm? Are the several outputs?

22. Subroutines that the algorithm uses

What subroutines provided by Ultimate are required? Ultimate provides e.g.,

• computation of sp and wp (for each the input is a predicate and a code block, the output is a predicate)
• equivalence check for predicates
• transformation from CFG to Petri net
• computation of finite prefix of the unfolding of a 1-safe Petri net
• after the preceding computation: the relations inCausalRelation, inCoRelation, inConflict

31. Precise Definition of the Reduction Rules

Most importantly, the Sequence rule, but also the Choice rule and optionally Fork/Join rules:

• How does it transform the Petri net?
• In which situations might it be applicable? Which arcs between involved places and transitions must exist, may exist, or may not exist? For the restrictions (some arcs may not exist), give a (possibly informal) reason why.
• What are the side conditions for the rules? Formulate them using the semantic relation. Which transitions are involved? Which mover conditions must be satisfied? Can some transitions be left- and others be right-movers, or do they all have to move in the same direction?

32. Cheap Sufficient Criteria for Side Conditions

The side conditions for the rules as defined on the semantic relations can be checked automatically. However, the general case is expensive (we need to check a logical formula). What are cheaper criteria that imply the side conditions?

• Restrictions on modified and used variables
• Possibly restrictions on types of statements: assume, havoc, assignment?
• If mover information about t1 and t2 is known and we fuse them to t1t2, what mover properties does the fused transition t1t2 have?

33. Pseudocode version of the Algorithm

The algorithm will probably consist of repeated application of the rules. However, there are some details to work out:

• Is there a specific order, or frequence, in which rules should be applied?
• How to find the places (and transitions) in a Petri net where a rule can be applied?

Literature

Petri nets

Petri nets on Wikipedia

Petri net unfoldings

1996TACAS - Esparza,Römer,Vogler - An Improvement of McMillan's Unfolding Algorithm

Textbook Unfoldings-Esparza-Heljanko

Semiar slides of Claus Schätzle

Program Verification (in general) via Trace Abstraction

Software Model Checking for People Who Love Automata

Poster zu Ultimate Automizer

Program Verification for Concurrent Programs via Trace Abstraction

Bachelorarbeit of Julian Jarecki