generalized async calls to allow their atomic action specification to be

left mover

Source/Concurrency/CivlRefinement.cs

@@ -141,6 +141,15 @@ public override Block VisitBlock(Block node)
         public override Cmd VisitCallCmd(CallCmd node)
         {
             CallCmd callCmd = (CallCmd) base.VisitCallCmd(node);
+            if (callCmd.IsAsync && civlTypeChecker.procToActionInfo.ContainsKey(node.Proc))
+            {
+                ActionInfo actionInfo = civlTypeChecker.procToActionInfo[node.Proc];
+                Debug.Assert(actionInfo.IsLeftMover);
+                if (actionInfo.createdAtLayerNum < layerNum)
+                {
+                    callCmd.IsAsync = false;
+                }
+            }
             callCmd.Proc = VisitProcedure(callCmd.Proc);
             callCmd.callee = callCmd.Proc.Name;
             absyMap[callCmd] = node;

Source/Concurrency/CivlTypeChecker.cs

@@ -785,7 +785,11 @@ public override Cmd VisitCallCmd(CallCmd node)
                 ActionInfo actionInfo = procToActionInfo[node.Proc];
                 if (node.IsAsync && actionInfo is AtomicActionInfo)
                 {
-                    Error(node, "Target of async call cannot be an atomic action");
+                    AtomicActionInfo atomicActionInfo = actionInfo as AtomicActionInfo;
+                    if (!atomicActionInfo.IsLeftMover)
+                    {
+                        Error(node, "Target of async call must be a left mover");
+                    }
                 }
                 int calleeLayerNum = procToActionInfo[node.Proc].createdAtLayerNum;
                 if (enclosingProcLayerNum < calleeLayerNum ||

Test/civl/async1.bpl

@@ -0,0 +1,14 @@
+// RUN: %boogie -noinfer -useArrayTheory "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+var {:layer 0} x: int;
+
+procedure {:yields} {:layer 0,1} Incr();
+ensures {:left} |{ L: x := x + 1; return true; }|;
+
+procedure {:yields} {:layer 1} AsyncIncr()
+ensures {:left} |{ L: x := x + 1; return true; }|;
+{
+  yield;
+  async call Incr();
+  yield;
+}

Test/civl/async1.bpl.expect

@@ -0,0 +1,2 @@
+
+Boogie program verifier finished with 2 verified, 0 errors