Sleep-Reduced Thread-Modular Proofs and related CHC refactoring #701
Conversation
This new implementation is meant to be easier to understand, extensible and modular. As an example, see the included implementation of sleep set reduction in the Horn clauses. The implementation is not yet completely finished, a few TODOs remain.
- ThreadModularHornClauseProvider: give params to individual methods, not constructor - ThreadModularHornClauseProvider: fix several bugs with generated clauses, e.g. transition constraints - HornClauseBuilder: default to not modifying variable unless explicitly stated (rather than the reverse) - HornClauseBuilder: support comments on clauses - ChcProviderConcurrent: use new Horn clause generation
Definition of the different kinds of clauses, and iteration over the Icfg are tightly coupled. Hence they are now managed by the same class.
For parametric programs, we can now generate CHC systems that encode correctness wrt a pre- / postcondition pair. The precondition should be annotated as a "free requires" on the thread template, Similarly, the postcondition should be annotated as a "free ensures".
# Conflicts: # releaseScripts/default/makeZip.sh # trunk/source/IcfgToChc/src/de/uni_freiburg/informatik/ultimate/plugins/icfgtochc/concurrent/ChcProviderConcurrentWithLbe.java
Move the creation of the symbolic independence relations to IndependenceChecker, and create a suitable symbol table for the relations as they work on instantiated conditions.
...e/ChcSolver/src/de/uni_freiburg/informatik/ultimate/plugins/chcsolver/ChcSolverObserver.java
Show resolved
Hide resolved
| } | ||
|
|
||
| private String getCommand(final File file) { | ||
| var command = "eld"; |
There was a problem hiding this comment.
This only works, if eld is in the PATH of the system, should we include an Eldarica build in releaseScripts?
There was a problem hiding this comment.
We need to make this a bit more portable, I agree.
eldis a bash script, so it won't work on Windows. It sets some parameters and then runs a JAR -- we should implement that directly.- Do we want to check in the eldarica JAR like we do for the SMT solver binaries, or wouldn't it be better to still have it as a Maven dependency?
I just thought about whether we could actually just call eldarica's main method from Java, but that might cause all kinds of unexpected behaviour (e.g. memory remaining allocated, re-invocations behaving incorrectly due to old cached stuff, coupling of required java versions), so... maybe not.
There was a problem hiding this comment.
Do we want to check in the eldarica JAR like we do for the SMT solver binaries, or wouldn't it be better to still have it as a Maven dependency?
Yes, the Maven dependency is much nicer of course. But I am not sure how you could actually call the binary in that case.
If it is not straightforward to include Eldarica in releaseScripts, we might really just assume that eld is in the PATH of the system for now (maybe you can throw an useful exception in that case?).
The best solution would be of course to get rid of EldaricaCliChcScript again and call Eldarica programmatically. If we cannot get it working, we could include the JAR along with our custom launchers (incl. for Windows) in releaseScripts. But this is more of a long term question 😉
...fgToChc/src/de/uni_freiburg/informatik/ultimate/plugins/icfgtochc/concurrent/HcLocalVar.java
Outdated
Show resolved
Hide resolved
...oChc/src/de/uni_freiburg/informatik/ultimate/plugins/icfgtochc/concurrent/HcLocationVar.java
Outdated
Show resolved
Hide resolved
| * @author Frank Schüssele ([email protected]) | ||
| * | ||
| */ | ||
| public class IcfgLiptonReducer { |
There was a problem hiding this comment.
Good idea to extract this to an own class 👍
As this this is independent of CHCs, can you move this to some other plugin (maybe Library-IcfgTransformer)?
There was a problem hiding this comment.
👍 I'll have a look
| .flatMap(e -> e.getValue().getIncomingEdges().stream() | ||
| .map(t -> new Triple<>(e.getKey(), t.getSource(), t.getTransformula()))) | ||
| .flatMap(e -> mInstances.stream().filter(i -> i.getTemplateName().equals(e.getFirst())) | ||
| .<Triple<ThreadInstance, IcfgLocation, UnmodifiableTransFormula>> map( |
There was a problem hiding this comment.
Is this type parameter necessary here?
| final var clause = createBuilder(mInvariantPredicate, "non-interference clause for transition " | ||
| + transition.hashCode() + " with transformula " + transition.getTransformula()); | ||
|
|
||
| // TODO support transitions with multiple predecessors (joins) |
There was a problem hiding this comment.
Does this TODO mean that we just ignore joins and thus overapproximate the behavior of the program here?
| public static final String LABEL_SYMMETRY_CLAUSES = "Use symmetry clauses"; | ||
| private static final boolean DEF_SYMMETRY_CLAUSES = false; | ||
|
|
||
| // TODO Currently unused |
There was a problem hiding this comment.
Are there any plans to use the settings right now?
| It is particularly recommended in connection with necessary-and-complete conditional independence."""; | ||
| private static final boolean DEF_NONDET_SLEEP_UPDATES = false; | ||
|
|
||
| // TODO Currently unused |
There was a problem hiding this comment.
Are there any plans to use the settings right now?
| } | ||
|
|
||
| public Derivation normalize(final Derivation derivation) { | ||
| // TODO |
There was a problem hiding this comment.
Is the normalization relevant for now?
Currently, the implementation does not work well: CHC systems that are easily solved by eldarica via the command line cannot be solved by this implementation. We are probably using the eldarica classes incorrectly. It's also not clear that eldarica provides a stable API, we are just accessing some implementation details here that might change at any time.
- document usage of different prime numbers for distinct hash codes - document purpose of classes - make implementations final - additional integrity checks (null checks, refined types of program variables) - updated & simplified equals()
This PR contains the integration of sleep set reduction for thread-modular proofs of concurrent programs, as described in our POPL'24 paper. It has been refactored to use the same symbolic independence relations introduced by PR #696.
The PR also contains the refactoring of program-to-CHC translation that was needed to implement the above techique without too much code duplication; and some fixes to our interfaces to CHC solvers.
➡️ @schuessf as you have worked on thread-modular proofs via CHC before, could you / do you want to take a look?