Refactor Event Semantics

dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/BranchEquivalence.java

@@ -229,9 +229,7 @@ private void computeBranchImplications(BranchDecomposition decomposition) {
                 final Branch creatorBranch = decomposition.event2BranchMap.get(start.getCreator());
                 threadInitialBranch.mustPred.add(creatorBranch);
                 threadInitialBranch.exclusiveBranches.addAll(creatorBranch.exclusiveBranches);
-                if (!start.mayFailSpuriously()) {
-                    creatorBranch.mustSucc.add(threadInitialBranch);
-                }
+                creatorBranch.mustSucc.add(threadInitialBranch);
             } else {
                 unconditionalThreadInitialBranches.add(threadInitialBranch);
             }

dartagnan/src/main/java/com/dat3m/dartagnan/program/event/AbstractEvent.java

@@ -1,6 +1,5 @@
 package com.dat3m.dartagnan.program.event;
 
-import com.dat3m.dartagnan.encoding.EncodingContext;
 import com.dat3m.dartagnan.program.Function;
 import com.dat3m.dartagnan.program.Program;
 import com.dat3m.dartagnan.program.Thread;
@@ -9,7 +8,6 @@
 import com.dat3m.dartagnan.program.event.metadata.MetadataMap;
 import com.dat3m.dartagnan.verification.Context;
 import com.google.common.base.Preconditions;
-import org.sosy_lab.java_smt.api.BooleanFormula;
 
 import java.util.*;
 
@@ -316,8 +314,4 @@ public boolean cfImpliesExec() {
         return !(this instanceof BlockingEvent);
     }
 
-    @Override
-    public BooleanFormula encodeExec(EncodingContext ctx) {
-        return ctx.getBooleanFormulaManager().makeTrue();
-    }
 }

dartagnan/src/main/java/com/dat3m/dartagnan/program/event/Event.java

@@ -1,12 +1,10 @@
 package com.dat3m.dartagnan.program.event;
 
-import com.dat3m.dartagnan.encoding.EncodingContext;
 import com.dat3m.dartagnan.program.Function;
 import com.dat3m.dartagnan.program.Program;
 import com.dat3m.dartagnan.program.Thread;
 import com.dat3m.dartagnan.program.event.metadata.Metadata;
 import com.dat3m.dartagnan.verification.Context;
-import org.sosy_lab.java_smt.api.BooleanFormula;
 
 import java.util.Collection;
 import java.util.List;
@@ -96,6 +94,4 @@ public interface Event extends Comparable<Event> {
 
     // This method needs to get overwritten for conditional events.
     boolean cfImpliesExec();
-
-    BooleanFormula encodeExec(EncodingContext ctx);
 }

dartagnan/src/main/java/com/dat3m/dartagnan/program/event/EventVisitor.java

@@ -6,12 +6,14 @@
 import com.dat3m.dartagnan.program.event.arch.vulkan.*;
 import com.dat3m.dartagnan.program.event.core.*;
 import com.dat3m.dartagnan.program.event.core.annotations.CodeAnnotation;
+import com.dat3m.dartagnan.program.event.core.threading.ThreadArgument;
 import com.dat3m.dartagnan.program.event.lang.catomic.*;
 import com.dat3m.dartagnan.program.event.lang.dat3m.NonDetChoice;
 import com.dat3m.dartagnan.program.event.lang.linux.*;
 import com.dat3m.dartagnan.program.event.lang.llvm.*;
 import com.dat3m.dartagnan.program.event.lang.spirv.*;
-import com.dat3m.dartagnan.program.event.lang.svcomp.*;
+import com.dat3m.dartagnan.program.event.lang.svcomp.BeginAtomic;
+import com.dat3m.dartagnan.program.event.lang.svcomp.EndAtomic;
 
 public interface EventVisitor<T> {
 
@@ -40,6 +42,8 @@ public interface EventVisitor<T> {
     // RMW core events
     default T visitRMWStore(RMWStore e) { return visitStore(e); }
     default T visitRMWStoreExclusive(RMWStoreExclusive e) { return visitStore(e); }
+    // Threading
+    default T visitThreadArgument(ThreadArgument e) { return visitEvent(e); }
     // Annotations
     default T visitCodeAnnotation(CodeAnnotation e) { return visitEvent(e); }
 

dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/Alloc.java

@@ -1,6 +1,5 @@
 package com.dat3m.dartagnan.program.event.core;
 
-import com.dat3m.dartagnan.encoding.EncodingContext;
 import com.dat3m.dartagnan.expression.Expression;
 import com.dat3m.dartagnan.expression.ExpressionFactory;
 import com.dat3m.dartagnan.expression.ExpressionVisitor;
@@ -15,7 +14,6 @@
 import com.dat3m.dartagnan.program.event.RegWriter;
 import com.dat3m.dartagnan.program.memory.MemoryObject;
 import com.google.common.base.Preconditions;
-import org.sosy_lab.java_smt.api.BooleanFormula;
 
 import java.math.BigInteger;
 import java.util.HashSet;
@@ -129,11 +127,4 @@ public <T> T accept(EventVisitor<T> visitor) {
         return visitor.visitAlloc(this);
     }
 
-    @Override
-    public BooleanFormula encodeExec(EncodingContext ctx) {
-        return ctx.getBooleanFormulaManager().and(
-                super.encodeExec(ctx),
-                ctx.getExpressionEncoder().assignEqualAt(ctx.result(this), this, getAllocatedObject(), this)
-        );
-    }
 }

dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/Assume.java

@@ -1,6 +1,5 @@
 package com.dat3m.dartagnan.program.event.core;
 
-import com.dat3m.dartagnan.encoding.EncodingContext;
 import com.dat3m.dartagnan.expression.Expression;
 import com.dat3m.dartagnan.expression.ExpressionVisitor;
 import com.dat3m.dartagnan.expression.type.BooleanType;
@@ -9,8 +8,6 @@
 import com.dat3m.dartagnan.program.event.EventVisitor;
 import com.dat3m.dartagnan.program.event.RegReader;
 import com.google.common.base.Preconditions;
-import org.sosy_lab.java_smt.api.BooleanFormula;
-import org.sosy_lab.java_smt.api.BooleanFormulaManager;
 
 import java.util.HashSet;
 import java.util.Set;
@@ -45,14 +42,6 @@ public String defaultString() {
         return "assume(" + expr + ")";
     }
 
-    @Override
-    public BooleanFormula encodeExec(EncodingContext ctx) {
-        BooleanFormulaManager bmgr = ctx.getBooleanFormulaManager();
-        return bmgr.and(
-                super.encodeExec(ctx),
-                bmgr.implication(ctx.execution(this), ctx.getExpressionEncoder().encodeBooleanAt(expr, this).formula()));
-    }
-
     @Override
     public void transformExpressions(ExpressionVisitor<? extends Expression> exprTransformer) {
         this.expr = expr.accept(exprTransformer);

dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/ControlBarrier.java

@@ -1,10 +1,8 @@
 package com.dat3m.dartagnan.program.event.core;
 
-import com.dat3m.dartagnan.encoding.EncodingContext;
 import com.dat3m.dartagnan.program.event.BlockingEvent;
 import com.dat3m.dartagnan.program.event.EventVisitor;
 import com.dat3m.dartagnan.program.event.Tag;
-import org.sosy_lab.java_smt.api.BooleanFormula;
 
 public class ControlBarrier extends GenericVisibleEvent implements BlockingEvent {
 
@@ -56,8 +54,4 @@ public <T> T accept(EventVisitor<T> visitor) {
         return visitor.visitControlBarrier(this);
     }
 
-    @Override
-    public BooleanFormula encodeExec(EncodingContext ctx) {
-        return ctx.getBooleanFormulaManager().implication(ctx.execution(this), ctx.controlFlow(this));
-    }
 }

dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/ExecutionStatus.java

@@ -1,18 +1,11 @@
 package com.dat3m.dartagnan.program.event.core;
 
-import com.dat3m.dartagnan.encoding.EncodingContext;
-import com.dat3m.dartagnan.encoding.ExpressionEncoder;
-import com.dat3m.dartagnan.expression.Expression;
 import com.dat3m.dartagnan.program.Register;
 import com.dat3m.dartagnan.program.event.*;
-import org.sosy_lab.java_smt.api.BooleanFormula;
-import org.sosy_lab.java_smt.api.BooleanFormulaManager;
 
 import java.util.Map;
 import java.util.Set;
 
-import static com.dat3m.dartagnan.encoding.ExpressionEncoder.ConversionMode.CAST;
-
 public class ExecutionStatus extends AbstractEvent implements RegWriter, EventUser {
 
     private Register register;
@@ -59,22 +52,6 @@ public String defaultString() {
         return register + " = not_exec(" + event + ")";
     }
 
-    @Override
-    public BooleanFormula encodeExec(EncodingContext context) {
-        final BooleanFormulaManager bmgr = context.getBooleanFormulaManager();
-        final ExpressionEncoder exprEncoder = context.getExpressionEncoder();
-
-        //TODO: We have "result == not exec(event)", because we use 0/false for executed events.
-        // The reason is that ExecutionStatus follows the behavior of Store-Conditionals on hardware.
-        // However, this is very counterintuitive and I think we should return 1/true on success and instead
-        // change the compilation of Store-Conditional to invert the value.
-        final Expression notExec = exprEncoder.wrap(bmgr.not(context.execution(event)));
-        return bmgr.and(
-                super.encodeExec(context),
-                context.getExpressionEncoder().assignEqual(context.result(this), notExec, CAST)
-        );
-    }
-
     @Override
     public Event getCopy() {
         return new ExecutionStatus(this);

dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/Local.java

@@ -1,6 +1,5 @@
 package com.dat3m.dartagnan.program.event.core;
 
-import com.dat3m.dartagnan.encoding.EncodingContext;
 import com.dat3m.dartagnan.expression.Expression;
 import com.dat3m.dartagnan.expression.ExpressionVisitor;
 import com.dat3m.dartagnan.program.Register;
@@ -9,7 +8,6 @@
 import com.dat3m.dartagnan.program.event.RegReader;
 import com.dat3m.dartagnan.program.event.RegWriter;
 import com.google.common.base.Preconditions;
-import org.sosy_lab.java_smt.api.BooleanFormula;
 
 import java.util.HashSet;
 import java.util.Set;
@@ -59,14 +57,6 @@ public String defaultString() {
         return String.format("%s = %s", register, expr);
     }
 
-    @Override
-    public BooleanFormula encodeExec(EncodingContext ctx) {
-        return ctx.getBooleanFormulaManager().and(
-                super.encodeExec(ctx),
-                ctx.getExpressionEncoder().assignEqualAt(ctx.result(this), this, expr, this)
-        );
-    }
-
     @Override
     public void transformExpressions(ExpressionVisitor<? extends Expression> exprTransformer) {
         this.expr = expr.accept(exprTransformer);

dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/RMWStoreExclusive.java

@@ -1,11 +1,9 @@
 package com.dat3m.dartagnan.program.event.core;
 
-import com.dat3m.dartagnan.encoding.EncodingContext;
 import com.dat3m.dartagnan.expression.Expression;
 import com.dat3m.dartagnan.program.event.Event;
 import com.dat3m.dartagnan.program.event.EventVisitor;
 import com.dat3m.dartagnan.program.event.Tag;
-import org.sosy_lab.java_smt.api.BooleanFormula;
 
 public class RMWStoreExclusive extends Store {
 
@@ -44,11 +42,6 @@ public String defaultString() {
         return String.format("%1$-" + Event.PRINT_PAD_EXTRA + "s", "excl " + super.defaultString()) + "# opt" + tag;
     }
 
-    @Override
-    public BooleanFormula encodeExec(EncodingContext ctx) {
-        return ctx.getBooleanFormulaManager().implication(ctx.execution(this), ctx.controlFlow(this));
-    }
-
     @Override
     public RMWStoreExclusive getCopy(){
         return new RMWStoreExclusive(this);

dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/threading/ThreadArgument.java

@@ -1,14 +1,8 @@
 package com.dat3m.dartagnan.program.event.core.threading;
 
-import com.dat3m.dartagnan.encoding.EncodingContext;
-import com.dat3m.dartagnan.expression.Expression;
 import com.dat3m.dartagnan.program.Register;
-import com.dat3m.dartagnan.program.event.AbstractEvent;
-import com.dat3m.dartagnan.program.event.Event;
-import com.dat3m.dartagnan.program.event.EventUser;
-import com.dat3m.dartagnan.program.event.RegWriter;
+import com.dat3m.dartagnan.program.event.*;
 import com.google.common.base.Preconditions;
-import org.sosy_lab.java_smt.api.BooleanFormula;
 
 import java.util.Map;
 import java.util.Set;
@@ -55,17 +49,6 @@ public String defaultString() {
         return String.format("%s = Argument(%s) from %s", register, argIndex, creator);
     }
 
-    @Override
-    public BooleanFormula encodeExec(EncodingContext context) {
-        final Expression equalValue = context.getExpressionFactory()
-                .makeEQ(context.result(this), creator.getArguments().get(argIndex));
-        return context.getBooleanFormulaManager().and(
-                super.encodeExec(context),
-                context.getExpressionEncoder().encodeBooleanAt(equalValue, creator).formula()
-        );
-    }
-
-
     @Override
     public ThreadArgument getCopy() {
         return new ThreadArgument(this);
@@ -80,4 +63,9 @@ public Set<Event> getReferencedEvents() {
     public void updateReferences(Map<Event, Event> updateMapping) {
         creator = (ThreadCreate) EventUser.moveUserReference(this, creator, updateMapping);
     }
+
+    @Override
+    public <T> T accept(EventVisitor<T> visitor) {
+        return visitor.visitThreadArgument(this);
+    }
 }

dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/threading/ThreadStart.java

@@ -9,16 +9,12 @@
 
 public class ThreadStart extends AbstractEvent implements EventUser {
 
-    // May be NULL, if this thread is not spawned.
+    // May be NULL if this thread is not spawned.
     private ThreadCreate creator;
-    //TODO: It is probably better to make the ThreadCreate conditional rather than
-    // allow ThreadStart to fail spuriously.
-    private boolean mayFailSpuriously;
 
     public ThreadStart(ThreadCreate creator) {
         this.creator = creator;
 
-        mayFailSpuriously = (creator != null);
         if (creator != null) {
             creator.registerUser(this);
         }
@@ -27,20 +23,18 @@ public ThreadStart(ThreadCreate creator) {
     protected ThreadStart(ThreadStart other) {
         super(other);
         this.creator = other.creator;
-        this.mayFailSpuriously = other.mayFailSpuriously;
 
-        creator.registerUser(this);
+        if (creator != null) {
+            creator.registerUser(this);
+        }
     }
 
-    public boolean mayFailSpuriously() { return mayFailSpuriously; }
-    public void setMayFailSpuriously(boolean value) { this.mayFailSpuriously = value;}
-
     public boolean isSpawned() { return creator != null; }
     public ThreadCreate getCreator() { return creator; }
 
     @Override
     public String defaultString() {
-        if ( isSpawned()) {
+        if (isSpawned()) {
             return String.format("ThreadStart by %s::%s", creator.getThread(), creator);
         } else {
             return "ThreadStart";

dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/CoreCodeVerification.java

@@ -2,6 +2,7 @@
 
 import com.dat3m.dartagnan.exception.MalformedProgramException;
 import com.dat3m.dartagnan.program.Function;
+import com.dat3m.dartagnan.program.ScopeHierarchy;
 import com.dat3m.dartagnan.program.event.Event;
 import com.dat3m.dartagnan.program.event.core.*;
 import com.dat3m.dartagnan.program.event.core.annotations.CodeAnnotation;
@@ -54,5 +55,28 @@ public void run(Function function) {
             }
             throw new MalformedProgramException("Found non-core events.\n" + msg);
         }
+
+        validateCoreEvents(function);
+    }
+
+    private void validateCoreEvents(Function function) {
+        StringBuilder msg = new StringBuilder();
+
+        for (ControlBarrier cb : function.getEvents(ControlBarrier.class)) {
+            // Check: Control barriers execution scopes match thread hierarchy
+            ScopeHierarchy hierarchy = cb.getThread().getScopeHierarchy();
+            if (hierarchy == null) {
+                msg.append(String.format("\t%2s: %-30s is not inside hierarchical thread %n", cb.getGlobalId(), cb));
+            } else {
+                final int id = hierarchy.getScopeId(cb.getExecScope());
+                if (id < 0) {
+                    msg.append(String.format("\t%2s: %-30s execution scope does not match thread hierarchy %n", cb.getGlobalId(), cb));
+                }
+            }
+        }
+
+        if (!msg.isEmpty()) {
+            throw new MalformedProgramException("Found errors in program.\n" + msg);
+        }
     }
 }