Merge Parallel Trace Abstraction into Dev #729
Conversation
- Adds Errorstates to each branch an annotates them with a TestGoal ID - Uses a BlockEncoding that breaks after Havoc NonDet - Long Trace Optimisation requiers some dependency changes - TraceCheck takes Value of the first representative and adds to a linkedList where the Index in the SSA corresponds to the index of the lsit - creates an ErrorAutomaton for every covered Testgoal along a Trace and saves the Result for each corresponding error State. - Writest All TestVectors in the same Folder - Writes MetaFile in WitnessPrinter
Activated Output
added doxtype to xmls
Fixed TestCase Ouput for negative numbers from (- 1) to -1
fixed floats
added dummy testcase
At the start in our serach we visit loops only once, hoping for more spred. During that time we only apply Craig interpolation Hoping to cover a large portion of the state space quick. When we no longer find cex we allow multiple per loop. Applying different assertion orders
after swtiching mode, search again
using futures too leads to sleeping twice Removed unused setting Fixed Bug in TraceCHeck affecting NWA
There was a problem hiding this comment.
Thanks for your work! Running trace abstraction in parallel can be really useful to reduce the walltime in practice (where we don't care about the CPU time).
I did not yet look into this PR in detail, but I have some more general comments.
I can see that it is complicated to manage scripts for different threads, but the current solution does not seem nice (it introduces some possibly unsafe casts) and complicates much of the existing code. Therefore, we should rather look for a more elegant solution before merging this PR.
| } | ||
| // Mapping in which that maps default TermVariables to their closed form (where | ||
| // variables are represented by inVars). Since array indices may also contain | ||
| // read-only variables we have to add from the inVars mapping. | ||
| final HashMap<TermVariable, Term> substitutionMapping = new HashMap<>(closedFormWithInvarsMap); | ||
| for (final IProgramVar pv : su.getReadonlyVars()) { | ||
| final Term oldValue = substitutionMapping.put(pv.getTermVariable(), inVars.get(pv)); | ||
| final Term oldValue = | ||
| substitutionMapping.put((TermVariable) ((HistoryRecordingScript) mgdScript.getScript()) |
There was a problem hiding this comment.
I think we should look for a better solution here. We should not cast every script to HistoryRecordingScript to access the method transferTermToWorker.
Also, where is it necessary to transfer the terms? It looks like many locations are affected, maybe there is also a more elegant solution for that.
There was a problem hiding this comment.
Yes a better solution would be great, so far i couldnt think of any.
We basically need it everywhere:
- Its necessary before we checksat or assert
- Before we build a formula we have to make sure the components are from the same script
- When we get a termVar representing a IProgramVar
- When we read a transformula, In, Out vars etc.
- When we create fresh predicates or use an old one
...burg/informatik/ultimate/lib/modelcheckerutils/cfg/transitions/UnmodifiableTransFormula.java
Outdated
Show resolved
Hide resolved
...te/plugins/generator/traceabstraction/preferences/TraceAbstractionPreferenceInitializer.java
Outdated
Show resolved
Hide resolved
|
Thanks for your work on this. Bringing parallelization to Ultimate is a big step, and it will be great to get it merged back into I think what we need here is an understanding for the architecture of your concurrent analysis, so that we can identify suitable interfaces between the workers and the main analysis thread. Then, the code can be refactored to handle all the business of this interaction -- primarily, it seems, the transferring of terms between scripts -- at well-defined points of these interfaces; such that separation of concerns is maintained. We already have some components in Ultimate using different scripts, perhaps they could serve as inspiration:
The current approach -- transferring these formulas in the most diverse set of classes, from loop acceleration over TermVarsFuns to SSA building code -- is extremely brittle. Who is to say that there is not some code path that is triggered only by few benchmarks, where the transferral is still missing? Any future change to Ultimate, e.g. some new kind of trace check, might introduce such cases. etc. I think we need a more robust solution. |
|
Sounds like a plan. You dont have to convince me that this needs some refactoring :) One thing we can do based on a suggestion of Matthias:
|
Adapted Parallel refinement strategy, now scales down after all assertion orders have been tried
IsEmptyParallel: We have to track the calls, I readded it, this might cause problems lets see, but without we cannot find cex in simple cases
|
That may be a possibility, but it introduces somewhat magic behaviour ;-) And you say it doesn't cover all cases. Is there a reason against simply transferring every object at the point where the object is handed from the main thread to a worker, or from a worker to the main thread? |
|
I was also thinking about something similar: |
…efore exploring new states, fixed unknown result in worker trace check
I prepared this branch to merge my parallel trace abstraction approach into main.
Feel free to take a look already, make suggestions, and ideally tell me how you want it to be refactored.
Unfortunately my changes affects quite a few classes.
Before merging, I need to run a few more experiments to ensure there are no unwanted side effects.
The following changes have been made:
ParallelNwaCegarLoop.java
Contains the main CEGAR loop
CegarNwaWorkerThread.java
Is the corresponding class that does the trace check, interpolation, and generalization of the resulting automton
ParallelRefinementStrategy
It not the same as for example CAMELRefinementStrategy, but its wrapper that provides modules to a BasicRefinementStrategy
depending on how often we have seen a PathProgram and how many worker threads are available.
IsEmptyParallel
A search strategy that gets a set of counterexamples as input. It tries to diverge from this set as soon as possible. After finding a prefix not in the set, it searches via BFS for the accepting state.
The biggest change, affecting most changed classes is related to scripts.
Every worker thread needs its own CFGscript. The original CFGscript i called MainScript.
When a worker is started it gets a copy (WorkerScript) of the MainScript.
The HistoryRecordingScript of the copy knows the MainScript and has a TermTransferrer to, on demand, transfer a term from main to worker. For example if we have IProgramVar.getTV().
This has the advantage that we only have one Transferrer and the HistoryRecordingScript can map TermVariables from Worker back to Main, such that we can obtain the corresponding IProgram vars.
We always and only transfer from Main to Worker. There is one exception, if we found a feasible counterexample and want to provide a program execution. Then we need to be able to translate the values, from Worker to Main to C.
This is done here
The second most changes come from Substitutions.
Here we have to make sure, the formula and both sides of the Subsitution mapping come from the worker script.
If you find a more elegant solution for Substitution and the HistoryRecordingScript let me know.