Added support for _Atomic variable

build.gradle.kts

@@ -29,7 +29,7 @@ buildscript {
 
 allprojects {
     group = "hu.bme.mit.theta"
-    version = "6.8.0"
+    version = "6.8.1"
 
     apply(from = rootDir.resolve("gradle/shared-with-buildSrc/mirrors.gradle.kts"))
 }

subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/grammar/expression/ExpressionVisitor.java

@@ -71,6 +71,7 @@ public class ExpressionVisitor extends CBaseVisitor<Expr<?>> {
     protected final List<CStatement> preStatements = new ArrayList<>();
     protected final List<CStatement> postStatements = new ArrayList<>();
     protected final Deque<Tuple2<String, Map<String, VarDecl<?>>>> variables;
+    protected final Set<VarDecl<?>> atomicVars;
     protected final Map<VarDecl<?>, CDeclaration> functions;
     private final ParseContext parseContext;
     private final FunctionVisitor functionVisitor;
@@ -80,13 +81,15 @@ public class ExpressionVisitor extends CBaseVisitor<Expr<?>> {
     private final Logger uniqueWarningLogger;
 
     public ExpressionVisitor(
+            Set<VarDecl<?>> atomicVars,
             ParseContext parseContext,
             FunctionVisitor functionVisitor,
             Deque<Tuple2<String, Map<String, VarDecl<?>>>> variables,
             Map<VarDecl<?>, CDeclaration> functions,
             TypedefVisitor typedefVisitor,
             TypeVisitor typeVisitor,
             Logger uniqueWarningLogger) {
+        this.atomicVars = atomicVars;
         this.parseContext = parseContext;
         this.functionVisitor = functionVisitor;
         this.variables = variables;
@@ -739,7 +742,8 @@ public Expr<?> visitGccPrettyFunc(CParser.GccPrettyFuncContext ctx) {
 
     @Override
     public Expr<?> visitPrimaryExpressionId(CParser.PrimaryExpressionIdContext ctx) {
-        return getVar(ctx.Identifier().getText()).getRef();
+        final var variable = getVar(ctx.Identifier().getText());
+        return variable.getRef();
     }
 
     @Override

subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/grammar/function/FunctionVisitor.java

@@ -38,7 +38,6 @@
 import hu.bme.mit.theta.core.type.arraytype.ArrayType;
 import hu.bme.mit.theta.core.type.booltype.BoolType;
 import hu.bme.mit.theta.frontend.ParseContext;
-import hu.bme.mit.theta.frontend.transformation.ArchitectureConfig;
 import hu.bme.mit.theta.frontend.transformation.ArchitectureConfig.ArithmeticType;
 import hu.bme.mit.theta.frontend.transformation.grammar.expression.ExpressionVisitor;
 import hu.bme.mit.theta.frontend.transformation.grammar.preprocess.ArithmeticTrait;
@@ -77,11 +76,13 @@ public class FunctionVisitor extends CBaseVisitor<CStatement> {
 
     public void clear() {
         variables.clear();
+        atomicVariables.clear();
         flatVariables.clear();
         functions.clear();
     }
 
     private final Deque<Tuple2<String, Map<String, VarDecl<?>>>> variables;
+    private final Set<VarDecl<?>> atomicVariables;
     private int anonCnt = 0;
     private final List<VarDecl<?>> flatVariables;
     private final Map<VarDecl<?>, CDeclaration> functions;
@@ -104,8 +105,6 @@ private String getName(final String name) {
     }
 
     private void createVars(String name, CDeclaration declaration, CComplexType type) {
-        //        checkState(declaration.getArrayDimensions().size() <= 1, "Currently, higher
-        // dimension arrays not supported");
         Tuple2<String, Map<String, VarDecl<?>>> peek = variables.peek();
         VarDecl<?> varDecl = Var(getName(name), type.getSmtType());
         if (peek.get2().containsKey(name)) {
@@ -115,6 +114,9 @@ private void createVars(String name, CDeclaration declaration, CComplexType type
         }
         peek.get2().put(name, varDecl);
         flatVariables.add(varDecl);
+        if (declaration.getType().isAtomic()) {
+            atomicVariables.add(varDecl);
+        }
         parseContext.getMetadata().create(varDecl.getRef(), "cType", type);
         parseContext.getMetadata().create(varDecl.getName(), "cName", name);
         declaration.addVarDecl(varDecl);
@@ -131,11 +133,13 @@ public FunctionVisitor(final ParseContext parseContext, Logger uniqueWarningLogg
         functions = new LinkedHashMap<>();
         this.parseContext = parseContext;
         globalDeclUsageVisitor = new GlobalDeclUsageVisitor(declarationVisitor);
+        atomicVariables = new LinkedHashSet<>();
     }
 
     @Override
     public CStatement visitCompilationUnit(CParser.CompilationUnitContext ctx) {
         variables.clear();
+        atomicVariables.clear();
         variables.push(Tuple2.of("", new LinkedHashMap<>()));
         flatVariables.clear();
         functions.clear();
@@ -148,7 +152,7 @@ public CStatement visitCompilationUnit(CParser.CompilationUnitContext ctx) {
 
         // if arithemetic is set on efficient, we change it to either bv or int arithmetic here
         if (parseContext.getArithmetic()
-                == ArchitectureConfig.ArithmeticType
+                == ArithmeticType
                         .efficient) { // if it wasn't on efficient, the check returns manual
             Set<ArithmeticTrait> arithmeticTraits =
                     BitwiseChecker.gatherArithmeticTraits(parseContext, globalUsages);
@@ -267,14 +271,24 @@ public CStatement visitFunctionDefinition(CParser.FunctionDefinitionContext ctx)
             CStatement accept = blockItemListContext.accept(this);
             variables.pop();
             CFunction cFunction =
-                    new CFunction(funcDecl, accept, new ArrayList<>(flatVariables), parseContext);
+                    new CFunction(
+                            funcDecl,
+                            accept,
+                            new ArrayList<>(flatVariables),
+                            parseContext,
+                            atomicVariables);
             recordMetadata(ctx, cFunction);
             return cFunction;
         }
         variables.pop();
         CCompound cCompound = new CCompound(parseContext);
         CFunction cFunction =
-                new CFunction(funcDecl, cCompound, new ArrayList<>(flatVariables), parseContext);
+                new CFunction(
+                        funcDecl,
+                        cCompound,
+                        new ArrayList<>(flatVariables),
+                        parseContext,
+                        atomicVariables);
         recordMetadata(ctx, cCompound);
         recordMetadata(ctx, cFunction);
         return cFunction;
@@ -315,6 +329,7 @@ public CStatement visitCaseStatement(CParser.CaseStatementContext ctx) {
                         ctx.constantExpression()
                                 .accept(
                                         new ExpressionVisitor(
+                                                atomicVariables,
                                                 parseContext,
                                                 this,
                                                 variables,
@@ -612,6 +627,7 @@ public CStatement visitAssignmentExpressionAssignmentExpression(
             CParser.AssignmentExpressionAssignmentExpressionContext ctx) {
         ExpressionVisitor expressionVisitor =
                 new ExpressionVisitor(
+                        atomicVariables,
                         parseContext,
                         this,
                         variables,
@@ -737,6 +753,7 @@ public CStatement visitConditionalExpression(CParser.ConditionalExpressionContex
 
         ExpressionVisitor expressionVisitor =
                 new ExpressionVisitor(
+                        atomicVariables,
                         parseContext,
                         this,
                         variables,

subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/model/statements/CFunction.java

@@ -13,27 +13,35 @@
  *  See the License for the specific language governing permissions and
  *  limitations under the License.
  */
-
 package hu.bme.mit.theta.frontend.transformation.model.statements;
 
 import hu.bme.mit.theta.core.decl.VarDecl;
 import hu.bme.mit.theta.frontend.ParseContext;
 import hu.bme.mit.theta.frontend.transformation.model.declaration.CDeclaration;
-
 import java.util.List;
+import java.util.Set;
 
 public class CFunction extends CStatement {
 
     private final CDeclaration funcDecl;
     private final CStatement compound;
     private final List<VarDecl<?>> flatVariables;
+    private final Set<VarDecl<?>> atomicVariables;
 
-    public CFunction(CDeclaration funcDecl, CStatement compound, List<VarDecl<?>> flatVariables, ParseContext parseContext) {
+    public CFunction(
+            CDeclaration funcDecl,
+            CStatement compound,
+            List<VarDecl<?>> flatVariables,
+            ParseContext parseContext,
+            Set<VarDecl<?>> atomicVariables) {
         super(parseContext);
         this.funcDecl = funcDecl;
         this.compound = compound;
         this.flatVariables = flatVariables;
-        parseContext.getMetadata().lookupMetadata(funcDecl)
+        this.atomicVariables = atomicVariables;
+        parseContext
+                .getMetadata()
+                .lookupMetadata(funcDecl)
                 .forEach((s, o) -> parseContext.getMetadata().create(this, s, o));
     }
 
@@ -53,4 +61,8 @@ public List<VarDecl<?>> getFlatVariables() {
     public <P, R> R accept(CStatementVisitor<P, R> visitor, P param) {
         return visitor.visit(this, param);
     }
+
+    public Set<VarDecl<?>> getAtomicVariables() {
+        return atomicVariables;
+    }
 }

subprojects/xcfa/c2xcfa/src/main/java/hu/bme/mit/theta/c2xcfa/FrontendXcfaBuilder.kt

@@ -106,7 +106,13 @@ class FrontendXcfaBuilder(
           "Not handling init expression of struct array ${globalDeclaration.get1()}",
         )
       }
-      builder.addVar(XcfaGlobalVar(globalDeclaration.get2(), type.nullValue))
+      builder.addVar(
+        XcfaGlobalVar(
+          globalDeclaration.get2(),
+          type.nullValue,
+          atomic = globalDeclaration.get1().type.isAtomic,
+        )
+      )
       if (type is CArray) {
         initStmtList.add(
           StmtLabel(
@@ -203,6 +209,7 @@ class FrontendXcfaBuilder(
   ): XcfaProcedureBuilder {
     locationLut.clear()
     val flatVariables = function.flatVariables
+    val isAtomic = function.atomicVariables::contains
     val funcDecl = function.funcDecl
     val compound = function.compound
     val builder =
@@ -238,6 +245,9 @@ class FrontendXcfaBuilder(
 
     for (flatVariable in flatVariables) {
       builder.addVar(flatVariable)
+      if (isAtomic(flatVariable)) {
+        builder.setAtomic(flatVariable)
+      }
       val type = CComplexType.getType(flatVariable.ref, parseContext)
       if (
         (type is CArray || type is CStruct) && builder.getParams().none { it.first == flatVariable }

subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaAnalysis.kt

@@ -228,9 +228,17 @@ fun getXcfaErrorPredicate(
             val mutexes2 = s.mutexes.filterValues { it == process2.key }.keys
             val globalVars1 = edge1.getGlobalVarsWithNeededMutexes(xcfa, mutexes1)
             val globalVars2 = edge2.getGlobalVarsWithNeededMutexes(xcfa, mutexes2)
-            for (v1 in globalVars1) for (v2 in globalVars2) if (v1.varDecl == v2.varDecl)
-              if (v1.access.isWritten || v2.access.isWritten)
-                if ((v1.mutexes intersect v2.mutexes).isEmpty()) return@Predicate true
+            for (v1 in globalVars1) {
+              for (v2 in globalVars2) {
+                if (
+                  v1.globalVar == v2.globalVar &&
+                    !v1.globalVar.atomic &&
+                    (v1.access.isWritten || v2.access.isWritten) &&
+                    (v1.mutexes intersect v2.mutexes).isEmpty()
+                )
+                  return@Predicate true
+              }
+            }
           }
         false
       }

subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/Utils.kt

@@ -121,6 +121,8 @@ typealias AccessType = Pair<Boolean, Boolean>
 
 typealias VarAccessMap = Map<VarDecl<*>, AccessType>
 
+typealias GlobalVarAccessMap = Map<XcfaGlobalVar, AccessType>
+
 val AccessType?.isRead
   get() = this?.first == true
 val AccessType?.isWritten
@@ -245,17 +247,21 @@ fun XcfaLabel.collectVarsWithAccessType(): VarAccessMap =
 /**
  * Returns the global variables accessed by the label (the variables present in the given argument).
  */
-private fun XcfaLabel.collectGlobalVars(globalVars: Set<VarDecl<*>>): VarAccessMap =
-  collectVarsWithAccessType().filter { labelVar -> globalVars.any { it == labelVar.key } }
+private fun XcfaLabel.collectGlobalVars(globalVars: Set<XcfaGlobalVar>): GlobalVarAccessMap =
+  collectVarsWithAccessType()
+    .mapNotNull { labelVar ->
+      globalVars.firstOrNull { it.wrappedVar == labelVar.key }?.let { Pair(it, labelVar.value) }
+    }
+    .toMap()
 
 /**
  * Returns the global variables (potentially indirectly) accessed by the edge. If the edge starts an
  * atomic block, all variable accesses in the atomic block are returned. Variables are associated
  * with a pair of boolean values: the first is true if the variable is read and false otherwise. The
  * second is similar for write access.
  */
-fun XcfaEdge.collectIndirectGlobalVarAccesses(xcfa: XCFA): VarAccessMap {
-  val globalVars = xcfa.globalVars.map(XcfaGlobalVar::wrappedVar).toSet()
+fun XcfaEdge.collectIndirectGlobalVarAccesses(xcfa: XCFA): GlobalVarAccessMap {
+  val globalVars = xcfa.globalVars
   val flatLabels = getFlatLabels()
   val mutexes =
     flatLabels.filterIsInstance<FenceLabel>().flatMap { it.acquiredMutexes }.toMutableSet()
@@ -271,7 +277,7 @@ fun XcfaEdge.collectIndirectGlobalVarAccesses(xcfa: XCFA): VarAccessMap {
  * (read/write) and the set of mutexes that are needed to perform the variable access.
  */
 class GlobalVarAccessWithMutexes(
-  val varDecl: VarDecl<*>,
+  val globalVar: XcfaGlobalVar,
   val access: AccessType,
   val mutexes: Set<String>,
 )
@@ -287,7 +293,7 @@ fun XcfaEdge.getGlobalVarsWithNeededMutexes(
   xcfa: XCFA,
   currentMutexes: Set<String>,
 ): List<GlobalVarAccessWithMutexes> {
-  val globalVars = xcfa.globalVars.map(XcfaGlobalVar::wrappedVar).toSet()
+  val globalVars = xcfa.globalVars
   val neededMutexes = currentMutexes.toMutableSet()
   val accesses = mutableListOf<GlobalVarAccessWithMutexes>()
   getFlatLabels().forEach { label ->
@@ -299,7 +305,7 @@ fun XcfaEdge.getGlobalVarsWithNeededMutexes(
         vars.mapNotNull { (varDecl, accessType) ->
           if (
             accesses.any {
-              it.varDecl == varDecl && (it.access == accessType && it.access == WRITE)
+              it.globalVar == varDecl && (it.access == accessType && it.access == WRITE)
             }
           ) {
             null
@@ -320,10 +326,10 @@ fun XcfaEdge.getGlobalVarsWithNeededMutexes(
  * @return the set of encountered shared objects
  */
 private fun XcfaEdge.collectGlobalVarsWithTraversal(
-  globalVars: Set<VarDecl<*>>,
+  globalVars: Set<XcfaGlobalVar>,
   goFurther: Predicate<XcfaEdge>,
-): VarAccessMap {
-  val vars = mutableMapOf<VarDecl<*>, AccessType>()
+): GlobalVarAccessMap {
+  val vars = mutableMapOf<XcfaGlobalVar, AccessType>()
   val exploredEdges = mutableListOf<XcfaEdge>()
   val edgesToExplore = mutableListOf<XcfaEdge>()
   edgesToExplore.add(this)

subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/model/Builders.kt

@@ -20,6 +20,7 @@ import hu.bme.mit.theta.core.type.Expr
 import hu.bme.mit.theta.core.type.Type
 import hu.bme.mit.theta.xcfa.passes.ProcedurePassManager
 import java.util.*
+import kotlin.collections.LinkedHashSet
 
 @DslMarker annotation class XcfaDsl
 
@@ -73,6 +74,7 @@ constructor(
   val manager: ProcedurePassManager,
   private val params: MutableList<Pair<VarDecl<*>, ParamDirection>> = ArrayList(),
   private val vars: MutableSet<VarDecl<*>> = LinkedHashSet(),
+  private val atomicVars: MutableSet<VarDecl<*>> = LinkedHashSet(),
   private val locs: MutableSet<XcfaLocation> = LinkedHashSet(),
   private val edges: MutableSet<XcfaEdge> = LinkedHashSet(),
   val metaData: MutableMap<String, Any> = LinkedHashMap(),
@@ -107,6 +109,14 @@ constructor(
       else -> vars
     }
 
+  fun VarDecl<*>.isAtomic() =
+    when {
+      this@XcfaProcedureBuilder::optimized.isInitialized -> optimized.atomicVars.contains(this)
+      this@XcfaProcedureBuilder::partlyOptimized.isInitialized ->
+        partlyOptimized.vars.contains(this)
+      else -> atomicVars.contains(this)
+    }
+
   fun getLocs(): Set<XcfaLocation> =
     when {
       this::optimized.isInitialized -> optimized.locs
@@ -182,6 +192,13 @@ constructor(
     vars.add(toAdd)
   }
 
+  fun setAtomic(v: VarDecl<*>) {
+    check(!this::optimized.isInitialized) {
+      "Cannot add/remove/modify elements after optimization passes!"
+    }
+    atomicVars.add(v)
+  }
+
   fun removeVar(toRemove: VarDecl<*>) {
     check(!this::optimized.isInitialized) {
       "Cannot add/remove new elements after optimization passes!"

subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/model/XCFA.kt

@@ -154,6 +154,7 @@ constructor(
   val wrappedVar: VarDecl<*>,
   val initValue: LitExpr<*>,
   val threadLocal: Boolean = false,
+  val atomic: Boolean = false,
 )
 
 enum class ParamDirection {