Skip to content

Commit

Permalink
moved handling of asyncs from YieldProcInstrumentation to YieldProcDu…
Browse files Browse the repository at this point in the history 
…plicator
  • Loading branch information
@shazqadeer
shazqadeer committed Mar 23, 2020
1 parent d58d2e7 commit 5399dcd
Show file tree
Hide file tree
Showing 2 changed files with 124 additions and 84 deletions.
160 changes: 109 additions & 51 deletions Source/Concurrency/YieldingProcDuplicator.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -17,6 +17,7 @@ public class YieldingProcDuplicator : Duplicator
private Dictionary<Absy, Absy> absyMap; /* Duplicate -> Original */
private Dictionary<Implementation, Implementation> implMap; /* Duplicate -> Original */
private HashSet<Procedure> yieldingProcs;
private Dictionary<string, Procedure> asyncCallPreconditionCheckers;

public YieldingProcDuplicator(CivlTypeChecker civlTypeChecker, LinearTypeChecker linearTypeChecker, int layerNum)
{
Expand All @@ -27,6 +28,7 @@ public YieldingProcDuplicator(CivlTypeChecker civlTypeChecker, LinearTypeChecker
this.absyMap = new Dictionary<Absy, Absy>();
this.implMap = new Dictionary<Implementation, Implementation>();
this.yieldingProcs = new HashSet<Procedure>();
this.asyncCallPreconditionCheckers = new Dictionary<string, Procedure>();
}

public override Procedure VisitProcedure(Procedure node)
Expand Down Expand Up @@ -245,61 +247,47 @@ private Variable CollectedPAs
}
}

private void ProcessCallCmd(CallCmd call, CallCmd newCall)
private void DesugarAsyncCall(CallCmd newCall)
{
if (civlTypeChecker.procToIntroductionProc.ContainsKey(call.Proc))
if (!asyncCallPreconditionCheckers.ContainsKey(newCall.Proc.Name))
{
if (!civlTypeChecker.CallExists(call, enclosingYieldingProc.upperLayer, layerNum))
return;
asyncCallPreconditionCheckers[newCall.Proc.Name] = new Procedure(Token.NoToken,
$"DummyAsyncTarget_{newCall.Proc.Name}",
newCall.Proc.TypeParameters, newCall.Proc.InParams, newCall.Proc.OutParams,
newCall.Proc.Requires, new List<IdentifierExpr>(), new List<Ensures>());
}
else
{
YieldingProc yieldingProc = civlTypeChecker.procToYieldingProc[call.Proc];
if (yieldingProc is SkipProc && yieldingProc.upperLayer < layerNum)
{
return;
}
if (newCall.IsAsync)
{
if ((call.HasAttribute(CivlAttributes.SYNC) && yieldingProc.upperLayer < layerNum) ||
(yieldingProc is MoverProc && yieldingProc.upperLayer == layerNum))
{
newCall.IsAsync = false;
}

if (yieldingProc is ActionProc actionProc && !call.HasAttribute(CivlAttributes.SYNC) && yieldingProc.upperLayer <= layerNum)
{
if (yieldingProc.upperLayer == layerNum)
{
newCmdSeq.Add(newCall);
}
if (!IsRefinementLayer) return;
if (SummaryHasPendingAsyncParam)
{
AtomicAction paAction;
if (actionProc.upperLayer == enclosingYieldingProc.upperLayer)
paAction = actionProc.refinedAction;
else
paAction = actionProc.RefinedActionAtLayer(layerNum);

var pa = ExprHelper.FunctionCall(paAction.pendingAsyncCtor, newCall.Ins.ToArray());
var inc = Expr.Add(Expr.Select(Expr.Ident(CollectedPAs), pa), Expr.Literal(1));
var add = CmdHelper.AssignCmd(CollectedPAs, Expr.Store(Expr.Ident(CollectedPAs), pa, inc));
newCmdSeq.Add(add);
}
else
{
newCmdSeq.Add(new AssertCmd(call.tok, Expr.False) { ErrorData = "This pending async is not summarized" });
}
return;
}
}
var dummyAsyncTargetProc = asyncCallPreconditionCheckers[newCall.Proc.Name];
CallCmd dummyCallCmd = new CallCmd(newCall.tok, dummyAsyncTargetProc.Name, newCall.Ins,
newCall.Outs, newCall.Attributes);
dummyCallCmd.Proc = dummyAsyncTargetProc;
newCmdSeq.Add(dummyCallCmd);
}

private void CollectPendingAsync(CallCmd call, CallCmd newCall, ActionProc actionProc)
{
if (SummaryHasPendingAsyncParam)
{
AtomicAction paAction;
if (actionProc.upperLayer == enclosingYieldingProc.upperLayer)
paAction = actionProc.refinedAction;
else
paAction = actionProc.RefinedActionAtLayer(layerNum);

InjectGate(yieldingProc, newCall);
var pa = ExprHelper.FunctionCall(paAction.pendingAsyncCtor, newCall.Ins.ToArray());
var inc = Expr.Add(Expr.Select(Expr.Ident(CollectedPAs), pa), Expr.Literal(1));
var add = CmdHelper.AssignCmd(CollectedPAs, Expr.Store(Expr.Ident(CollectedPAs), pa, inc));
newCmdSeq.Add(add);
}
else
{
newCmdSeq.Add(new AssertCmd(call.tok, Expr.False)
{ErrorData = "This pending async is not summarized"});
}
}

newCmdSeq.Add(newCall);

private void CollectPendingAsyncs(CallCmd call, CallCmd newCall)
{
// Inject pending async collection
if (newCall.Outs.Count != newCall.Proc.OutParams.Count)
{
Expand All @@ -308,7 +296,8 @@ private void ProcessCallCmd(CallCmd call, CallCmd newCall)
if (!IsRefinementLayer) return;
if (SummaryHasPendingAsyncParam)
{
var collectedUnionReturned = ExprHelper.FunctionCall(civlTypeChecker.pendingAsyncAdd, Expr.Ident(CollectedPAs), Expr.Ident(ReturnedPAs));
var collectedUnionReturned = ExprHelper.FunctionCall(civlTypeChecker.pendingAsyncAdd,
Expr.Ident(CollectedPAs), Expr.Ident(ReturnedPAs));
newCmdSeq.Add(CmdHelper.AssignCmd(CollectedPAs, collectedUnionReturned));
}
else
Expand All @@ -318,12 +307,81 @@ private void ProcessCallCmd(CallCmd call, CallCmd newCall)
var paBound = VarHelper.BoundVariable("pa", civlTypeChecker.pendingAsyncType);
var pa = Expr.Ident(paBound);
var expr = Expr.Eq(Expr.Select(Expr.Ident(ReturnedPAs), pa), Expr.Literal(0));
var forallExpr = new ForallExpr(Token.NoToken, new List<Variable> { paBound }, expr);
var forallExpr = new ForallExpr(Token.NoToken, new List<Variable> {paBound}, expr);
forallExpr.Typecheck(new TypecheckingContext(null));
newCmdSeq.Add(new AssertCmd(call.tok, forallExpr) { ErrorData = "Pending asyncs created by this call are not summarized" });
newCmdSeq.Add(new AssertCmd(call.tok, forallExpr)
{ErrorData = "Pending asyncs created by this call are not summarized"});
}
}
}

private void ProcessCallCmd(CallCmd call, CallCmd newCall)
{
if (civlTypeChecker.procToIntroductionProc.ContainsKey(call.Proc))
{
if (civlTypeChecker.CallExists(call, enclosingYieldingProc.upperLayer, layerNum))
{
newCmdSeq.Add(newCall);
}
return;
}

// handle calls to yielding procedures in the rest of this method
YieldingProc yieldingProc = civlTypeChecker.procToYieldingProc[call.Proc];

if (newCall.IsAsync)
{
if (yieldingProc.upperLayer < layerNum)
{
if (call.HasAttribute(CivlAttributes.SYNC))
{
// synchronize the called atomic action
newCall.IsAsync = false;
newCmdSeq.Add(newCall);
}
}
else
{
if (yieldingProc is MoverProc && yieldingProc.upperLayer == layerNum)
{
// synchronize the called mover procedure
newCall.IsAsync = false;
newCmdSeq.Add(newCall);
}
else
{
DesugarAsyncCall(newCall);
if (IsRefinementLayer && yieldingProc is ActionProc actionProc)
{
CollectPendingAsync(call, newCall, actionProc);
}
}
}
return;
}

// handle synchronous calls to skip procedures
if (yieldingProc is SkipProc)
{
if (yieldingProc.upperLayer >= layerNum)
{
newCmdSeq.Add(newCall);
}
return;
}

// handle synchronous calls to mover procedures
if (yieldingProc is MoverProc)
{
newCmdSeq.Add(newCall);
return;
}

// handle synchronous calls to action procedures
InjectGate(yieldingProc, newCall);
newCmdSeq.Add(newCall);
CollectPendingAsyncs(call, newCall);
}

private void ProcessParCallCmd(ParCallCmd parCall, ParCallCmd newParCall)
{
Expand Down
48 changes: 15 additions & 33 deletions Source/Concurrency/YieldingProcInstrumentation.cs
View file
Original file line number Diff line number Diff line change
@@ -1,5 +1,6 @@
using System;
using System.Collections.Generic;
using System.Diagnostics;
using System.Linq;
using System.Diagnostics.Contracts;
using Microsoft.Boogie.GraphUtil;
Expand Down Expand Up @@ -30,7 +31,7 @@ public static List<Declaration> TransformImplementations(
}

List<Declaration> decls = new List<Declaration>(yieldingProcInstrumentation.yieldCheckerDecls);
foreach (Procedure proc in yieldingProcInstrumentation.asyncAndParallelCallDesugarings.Values)
foreach (Procedure proc in yieldingProcInstrumentation.parallelCallPreconditionCheckers.Values)
{
decls.Add(proc);
}
Expand All @@ -53,7 +54,7 @@ private YieldingProcInstrumentation(
this.absyMap = absyMap;
this.implMap = implMap;
this.yieldingProcs = yieldingProcs;
asyncAndParallelCallDesugarings = new Dictionary<string, Procedure>();
parallelCallPreconditionCheckers = new Dictionary<string, Procedure>();
yieldCheckerDecls = new List<Declaration>();

List<Variable> inputs = new List<Variable>();
Expand All @@ -79,7 +80,7 @@ private YieldingProcInstrumentation(
private Dictionary<Implementation, Implementation> implMap;
private HashSet<Procedure> yieldingProcs;

private Dictionary<string, Procedure> asyncAndParallelCallDesugarings;
private Dictionary<string, Procedure> parallelCallPreconditionCheckers;
private List<Declaration> yieldCheckerDecls;
private Procedure yieldProc;

Expand Down Expand Up @@ -384,37 +385,18 @@ private void DesugarConcurrency(Implementation impl)
else if (cmd is CallCmd callCmd && yieldingProcs.Contains(callCmd.Proc))
{
List<Cmd> newCmds = new List<Cmd>();
if (callCmd.IsAsync)
if (!blocksInYieldingLoops.Contains(b))
{
if (!asyncAndParallelCallDesugarings.ContainsKey(callCmd.Proc.Name))
{
asyncAndParallelCallDesugarings[callCmd.Proc.Name] = new Procedure(Token.NoToken,
$"DummyAsyncTarget_{callCmd.Proc.Name}",
callCmd.Proc.TypeParameters, callCmd.Proc.InParams, callCmd.Proc.OutParams,
callCmd.Proc.Requires, new List<IdentifierExpr>(), new List<Ensures>());
}

var dummyAsyncTargetProc = asyncAndParallelCallDesugarings[callCmd.Proc.Name];
CallCmd dummyCallCmd = new CallCmd(callCmd.tok, dummyAsyncTargetProc.Name, callCmd.Ins,
callCmd.Outs, callCmd.Attributes);
dummyCallCmd.Proc = dummyAsyncTargetProc;
newCmds.Add(dummyCallCmd);
newCmds.AddRange(refinementInstrumentation.CreateUpdatesToRefinementVars());
}
else
newCmds.Add(callCmd);
if (civlTypeChecker.sharedVariables.Count > 0)
{
if (!blocksInYieldingLoops.Contains(b))
{
newCmds.AddRange(refinementInstrumentation.CreateUpdatesToRefinementVars());
}
newCmds.Add(callCmd);
if (civlTypeChecker.sharedVariables.Count > 0)
{
newCmds.AddRange(refinementInstrumentation.CreateAssumeCmds());
}
newCmds.AddRange(globalSnapshotInstrumentation.CreateUpdatesToOldGlobalVars());
newCmds.AddRange(refinementInstrumentation.CreateUpdatesToOldOutputVars());
newCmds.AddRange(noninterferenceInstrumentation.CreateUpdatesToPermissionCollector(callCmd));
newCmds.AddRange(refinementInstrumentation.CreateAssumeCmds());
}
newCmds.AddRange(globalSnapshotInstrumentation.CreateUpdatesToOldGlobalVars());
newCmds.AddRange(refinementInstrumentation.CreateUpdatesToOldOutputVars());
newCmds.AddRange(noninterferenceInstrumentation.CreateUpdatesToPermissionCollector(callCmd));
newCmds.AddRange(b.cmds.GetRange(1, b.cmds.Count - 1));
b.cmds = newCmds;
}
Expand Down Expand Up @@ -592,7 +574,7 @@ private List<Cmd> DesugarParCallCmd(ParCallCmd parCallCmd)
outs.AddRange(callCmd.Outs);
}

if (!asyncAndParallelCallDesugarings.ContainsKey(procName))
if (!parallelCallPreconditionCheckers.ContainsKey(procName))
{
List<Variable> inParams = new List<Variable>();
List<Variable> outParams = new List<Variable>();
Expand Down Expand Up @@ -628,12 +610,12 @@ private List<Cmd> DesugarParCallCmd(ParCallCmd parCallCmd)
}
count++;
}
asyncAndParallelCallDesugarings[procName] = new Procedure(Token.NoToken, procName,
parallelCallPreconditionCheckers[procName] = new Procedure(Token.NoToken, procName,
new List<TypeVariable>(), inParams, outParams, requiresSeq,
civlTypeChecker.sharedVariableIdentifiers, ensuresSeq);
}

Procedure proc = asyncAndParallelCallDesugarings[procName];
Procedure proc = parallelCallPreconditionCheckers[procName];
CallCmd dummyCallCmd = new CallCmd(parCallCmd.tok, proc.Name, ins, outs, parCallCmd.Attributes);
dummyCallCmd.Proc = proc;
newCmds.Add(dummyCallCmd);
Expand Down

0 comments on commit 5399dcd

Please sign in to comment.