Skip to content

Large Block Encoding for Concurrent Programs

Jump to bottom
Matthias Heizmann edited this page Oct 29, 2019 · 19 revisions

Large Block Encoding for Concurrent Programs

Tasks

Finished

1. Pre-Analysis.

Briefly read the literature to get a coarse idea of the topic. This step is necessary in order to write the proposal.

2. Write a Proposal.

Write a proposal to introduce the topic and why it might be helpful to have an algorithm that performs Large Block Encoding on concurrent programs. This is very helpful to get a basic overview on the topic. It is not necessary to have a detailed idea about everything yet.

3. Literature Analysis.

Analyze the literature that is related to the Thesis. This is necessary for any of the next steps.

4. Sequential Composition of Statements: Criteria.

Determine the Criteria necessary to perform Large Block Encoding on concurrent programs. This forms the base of the Algorithm. It is necessary to understand the concept of left and right movers in order to determine the criteria. This is the base for the Precise Definition of the Reduction Rules.

5. Kickoff Meeting.

Preparing the slides for the Kickoff Meeting. Give a talk about the topic explaining why Large Block Encoding for Concurrent Programs is an interesting topic and explain how it will be performed.

6. Ultimate Setup.

Install Ultimate on the device. This might take some time.

7. Use the developer GUI in Ultimate to analyze a program.

Examples in trunk/examples/concurrent/ Toolchain trunk/examples/toolchains/PetriAutomizerBplInline.xml or trunk/examples/toolchains/PetriAutomizerCInline.xml This step is necessary in order to get to know how to work with Ultimate.

8. 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).

9. Write Boogie programs.

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

10. 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. Demonstrate somehow that large block encoding is speeding up automata operations.

11. 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?
  • 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)

TODO

12. SV-COMP benchmarks

Get the pthread benchmarks from the SV-COMP https://sv-comp.sosy-lab.org/2019/ and verify one of these. Use settings trunk/examples/settings/default/automizer/svcomp-Reach-32bit-Automizer_Default.epf

13. Define the term CoEnable.

This definition is necessary to have in order to write the algorithm. We have to introduce this new definition because the term 'concurrent' is only defined in occurrence nets (in the unfolding of a Petri Net) and we need to access the pairs of transitions where there exists one corresponding pair of events in the Unfolding which is in co-relation.

14. 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? This is an iterative process: the first version is

15. Inputs and Outputs of the algorithm

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

16. 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

17. Proving D-Reduction from the Lipton Paper.

Show that fusing an entire sequence (as in the Lipton paper) can be split into repeatedly fusing just two transitions.

18. (Hopefully) Proving coEnabled.

19. Implementing the algorithm to the Ultimate tool.

This step is necessary in order to be able to perform the Large Block Encoding.

20. Evaluating the algorithm.

Find examples where the algorithm is (very) helpful and also examples where the algorithm doesn't help at all.

21. Writing the thesis.

Writing the actual thesis. This is the most important step of all. Possible outline (maybe not complete yet):

  1. Introduction
  2. Related Work
  3. Concurrent Programs
  4. Petri Nets (Important Definitions, like: occurrence net, marking, unfolding, pre- & postset, coEnabled, ..., Petri Nets in Boogie)
  5. Reduction (Left and Right movers; D-Reduction)
  6. Single- and Large Block Encoding for concurrent programs (Comparison, explaining LBE for concurrent programs)

22. Preparing the final presentation.

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.

Verify a concurrent program with Ultimate Automizer

We have two different analyses that can verify concurrent programs. Currently these analyses are not selected via the settings but via the toolchain.

  • The toolchain trunk/examples/toolchains/PetriAutomizerCInline.xml (resp. trunk/examples/toolchains/PetriAutomizerBplInline.xml) uses an analysis that is completely based on Petri net.
  • The toolchain trunk/examples/toolchains/AutomizerCInline.xml (resp. trunk/examples/toolchains/AutomizerBplInline.xml) uses an analysis that translates the Petri net into a finite automaton after the LBE.

See details of verification run

  • Start Ultimate GUI in Eclipse's debug mode
  • The verification starts in class TraceAbstractionConcurrentObserver
  • Set breakpoint
  • Open some example, e.g., a boogie program from trunk/examples/concurrent/concurrentBoogie/
  • Use a toolchain trunk/examples/toolchains/PetriAutomizerBplInline.xml for Boogie programs and trunk/examples/toolchains/PetriAutomizerCInline.xmlfor C programs
  • Verification run should stop at breakpoint
  • On the right you can see all variables in the current scope and the result of their toString() method.
  • If you want to run code while observing the verification run, you can use Window -> Show View -> Display

Test implementation on several files

  • Use class PetriAutomizerTest
  • Class is hopefully self-explaining. Add/remove folders/setting/toolchains that you like/dislike. Change timeout.
  • There are currently two preference files. One with LBE, one without LBE.
  • Do not commit your changes unless they are useful for everyone.
  • Right click to get context menu -> Run as -> JUnit Plug-in Test
  • Alternative: "Debug as" instead of "Run as". Note that timouts < 10 hours can hamper your debugging actvities
  • Logs and test summaries are written to trunk/source/UltimateTest/target/surefire-reports/de.uni_freiburg.informatik.ultimate.ultimatetest.suites.traceabstraction.PetriAutomizerTest/
  • If you want to have more tests than add more .bpl files to the repository. Add subfolders if you like. Use the keyword #Safe or #Unsafe in the first line of each file to indicate your expected result.

Relevant classes/interfaces in Ultimate

  • IcfgEdge default implementation of an IIcfgTransition. Use IcfgEdgeFactory to construct IcfgEdges.
  • IIcfgTransition edge/transition of an ICFG. In the trace abstraction algorithm, the alphabet (of the automata) is the set of all program statements. In our implementation, the alphabet is the set of all IIcfgTransitions.
  • ITransition interface that represents transitions of a Petri net. See class documentation. Objects that implement this class should only be constructed by the Petri net that has this transitions. See e.g., BoundedPetriNet#addTransition

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

K. McMillan: A Technique of State Space Search Based on Unfolding

Seminar slides of Claus Schätzle

Reduction

Reduction: A Method of Proving Properties of Parallel Programs

A Calculus of Atomic Actions

Large Block Encoding

Software Model Checking via Large Block Encoding

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