Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Sleep-Reduced Thread-Modular Proofs and related CHC refactoring #701

Draft
wants to merge 123 commits into
base: dev
Choose a base branch
from

Conversation

maul-esel
Copy link
Contributor

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?

maul-esel added 30 commits April 1, 2023 12:59
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.
@maul-esel maul-esel requested review from schuessf and ebbima January 3, 2025 15:42
Copy link
Contributor

@schuessf schuessf left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks for your work! Your changes drastically improve the code (that was rather ad-hoc by me 😄). I have just a few comments left.

}

private String getCommand(final File file) {
var command = "eld";
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This only works, if eld is in the PATH of the system, should we include an Eldarica build in releaseScripts?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

We need to make this a bit more portable, I agree.

  • eld is 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.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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 😉

* @author Frank Schüssele ([email protected])
*
*/
public class IcfgLiptonReducer {
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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)?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

👍 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(
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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)
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Are there any plans to use the settings right now?

}

public Derivation normalize(final Derivation derivation) {
// TODO
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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()
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants