-
Notifications
You must be signed in to change notification settings - Fork 41
Large Block Encoding for Concurrent Programs
Briefly read the literature to get a coarse idea of the topic. This step is necessary in order to write the 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.
Analyze the literature that is related to the Thesis. This is necessary for any of the next steps.
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.
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.
Install Ultimate on the device. This might take some time.
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.
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).
Write two new concurrent Boogie programs (one safe/one unsafe) that are related to your thesis.
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.
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
t1andt2is known and we fuse them (with the Sequence rule) tot1t2, what mover properties does the fused transitiont1t2have? What if we fuse them with the Choice rule, tot1 || 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)
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
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.
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
What are the inputs and outputs of the algorithm? Are the several outputs?
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
Show that fusing an entire sequence (as in the Lipton paper) can be split into repeatedly fusing just two transitions.
This step is necessary in order to be able to perform the Large Block Encoding.
Find examples where the algorithm is (very) helpful and also examples where the algorithm doesn't help at all.
Writing the actual thesis. This is the most important step of all. Possible outline (maybe not complete yet):
- Introduction
- Related Work
- Concurrent Programs
- Petri Nets (Important Definitions, like: occurrence net, marking, unfolding, pre- & postset, coEnabled, ..., Petri Nets in Boogie)
- Reduction (Left and Right movers; D-Reduction)
- Single- and Large Block Encoding for concurrent programs (Comparison, explaining LBE for concurrent programs)
- Write Petri net definition in automata script syntax (examples are in
trunk/examples/Automata/PetriNet/andtrunk/examples/Automata/regression/pn/) - Use command
finitePrefixto 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.
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.
- 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.xmlfor Boogie programs andtrunk/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
- 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.
In the subfolders of trunk/source/UltimateTest/target/surefire-reports/ you find several files. These are meant for the following.
-
StandingsSummarywhich settings/toolchain pair performs best measured in total numbers -
KingOfTheHillSummarywhich settings/toolchain pair performs best measured in subsets of benchmarks (in general not a total order) -
IncrementalLogWithBenchmarkResultsresults for individual file/settings/toolchain triples in human readable form -
CsvPetriNetLargeBlockEncodingBenchmarksbenchmark results for LBE in machine readable form (humans have to use libreoffice or some other tool for processing spreadsheets)
- 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
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: A Method of Proving Properties of Parallel Programs
Software Model Checking via Large Block Encoding
Software Model Checking for People Who Love Automata
Bachelorarbeit of Julian Jarecki
- Home
- Ultimate Development
- Ultimate Build System
- Documentation
- Project Topics