Skip to content

Large Block Encoding for Concurrent Programs

Jump to bottom
Matthias Heizmann edited this page Aug 3, 2019 · 19 revisions

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? (Last point: no. Give a short counterexample).

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 (with the Sequence rule) to t1t2, what mover properties does the fused transition t1t2 have? What if we fuse them with the Choice rule, to t1 || t2?
  • As consequence of the previous point: Show that fusing an entire sequence (as in the Lipton paper) can be split into repeatedly fusing just two transitions.
  • If mover properties are known, and a rule is applied, how do they change? How does the co-relation of the Petri net change, can we compute it easily, without computing the unfolding prefix again? (Question for Matthias)

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?

How-to

Use Automata Script Library to show co-relation for unfoldings

  • Write Petri net definition in automata script syntax (examples are in trunk/examples/Automata/PetriNet/ and trunk/examples/Automata/regression/pn/)
  • Use command finitePrefix to compute finite prefix of an unfolding
  • Use print(x) command to see x
  • Unfortunately, the textual representation of a branching process does not seem to work at the moment
  • The Jung graph visualization in Ultimate visualizes the argument of the last print command as a graph.
  • The Jung graph visualization is only available in the (debug) GUI and not in the web interface.
  • Use the toolchain trunk/examples/toolchains/AutomataScriptInterpreterWithJung.xml
  • Click on conditions to see the list of co-related conditions in the "node view"
  • Never close the node view, we cannot recover it. If you closed it you have to delete the .ultimate subfolder in your home directory.

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

Clone this wiki locally