Skip to content

Commit

Permalink
[Civl] Add support for skip async calls (#923)
Browse files Browse the repository at this point in the history 
Co-authored-by: Shaz Qadeer <[email protected]>
  • Loading branch information
@shazqadeer
shazqadeer and Shaz Qadeer authored Jul 30, 2024
1 parent 02fd4a3 commit b5ea010
Show file tree
Hide file tree
Showing 6 changed files with 110 additions and 50 deletions.
18 changes: 16 additions & 2 deletions Source/Concurrency/YieldingProcDuplicator.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -297,7 +297,15 @@ private void ProcessCallCmd(CallCmd newCall)
}
else if (IsRefinementLayer)
{
AddPendingAsync(newCall, yieldingProc);
if (newCall.HasAttribute(CivlAttributes.SKIP))
{
var calleeRefinedAction = PrepareNewCall(newCall, yieldingProc);
InjectGate(calleeRefinedAction, newCall);
}
else
{
AddPendingAsync(newCall, yieldingProc);
}
}
}
else
Expand Down Expand Up @@ -406,7 +414,7 @@ private void ProcessParCallCmd(ParCallCmd newParCall)
}
}

private void AddActionCall(CallCmd newCall, YieldProcedureDecl calleeActionProc)
private Action PrepareNewCall(CallCmd newCall, YieldProcedureDecl calleeActionProc)
{
var calleeRefinedAction = civlTypeChecker.Action(calleeActionProc.RefinedActionAtLayer(layerNum));

Expand Down Expand Up @@ -438,6 +446,12 @@ private void AddActionCall(CallCmd newCall, YieldProcedureDecl calleeActionProc)
newCall.Ins = newIns;
newCall.Outs = newOuts;

return calleeRefinedAction;
}

private void AddActionCall(CallCmd newCall, YieldProcedureDecl calleeActionProc)
{
var calleeRefinedAction = PrepareNewCall(newCall, calleeActionProc);
InjectGate(calleeRefinedAction, newCall, !IsRefinementLayer);
newCmdSeq.Add(newCall);

Expand Down
11 changes: 9 additions & 2 deletions Source/Core/AST/Absy.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3166,6 +3166,15 @@ public IEnumerable<ActionDeclRef> ActionDeclRefs()
return Creates.Append(RefinedAction).Append(InvariantAction);
}

public bool IsSkippable()
{
return
Creates.Count == 0 &&
ModifiedVars.All(v => v.LayerRange.UpperLayer == LayerRange.UpperLayer) &&
Asserts.Count > 0 &&
!VariableCollector.Collect(Asserts).Any(v => v is GlobalVariable);
}

public IEnumerable<ActionDecl> CreateActionDecls => Creates.Select(x => x.ActionDecl);

public bool MaybePendingAsync => PendingAsyncCtorDecl != null;
Expand Down Expand Up @@ -3415,10 +3424,8 @@ public ActionDecl RefinedActionAtLayer(int layer)
{
return actionDecl;
}

actionDeclRef = actionDecl.RefinedAction;
}

return null;
}

Expand Down
98 changes: 53 additions & 45 deletions Source/Core/AST/CallCmd.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -301,6 +301,7 @@ void CheckModifies(IEnumerable<Variable> modifiedVars)
if (Proc is YieldProcedureDecl calleeDecl)
{
var isSynchronized = this.HasAttribute(CivlAttributes.SYNC);
var isSkipped = this.HasAttribute(CivlAttributes.SKIP);
if (calleeDecl.Layer > callerDecl.Layer)
{
tc.Error(this, "layer of callee must not be more than layer of caller");
Expand All @@ -319,33 +320,58 @@ void CheckModifies(IEnumerable<Variable> modifiedVars)
else
{
CheckModifies(highestRefinedActionDecl.ModifiedVars);
if (highestRefinedActionDecl.Creates.Any())
if (!IsAsync)
{
if (callerDecl.HasMoverType)
if (highestRefinedActionDecl.Creates.Any() && callerDecl.HasMoverType)
{
tc.Error(this, "caller must not be a mover procedure");
}
// check there is no application of IS_RIGHT in the entire chain of refined actions
var calleeRefinedAction = calleeDecl.RefinedAction;
while (calleeRefinedAction != null)
{
if (calleeRefinedAction.HasAttribute(CivlAttributes.IS_RIGHT))
{
tc.Error(this, "this must be an async call");
break;
}
var calleeActionDecl = calleeRefinedAction.ActionDecl;
if (calleeActionDecl == highestRefinedActionDecl)
{
break;
}
calleeRefinedAction = calleeActionDecl.RefinedAction;
}
}
else if (IsAsync && isSynchronized)
else if (isSynchronized)
{
// check that entire chain of refined actions all the way to highestRefinedAction is comprised of left movers
var actionDeclRef = calleeDecl.RefinedAction;
while (actionDeclRef != null)
var calleeRefinedAction = calleeDecl.RefinedAction;
while (calleeRefinedAction != null)
{
var actionDecl = actionDeclRef.ActionDecl;
if (!actionDecl.IsLeftMover)
var calleeActionDecl = calleeRefinedAction.ActionDecl;
if (!calleeActionDecl.IsLeftMover)
{
tc.Error(this,
$"callee abstraction in synchronized call must be a left mover: {actionDecl.Name}");
}
else if (actionDecl != highestRefinedActionDecl)
{
actionDeclRef = actionDecl.RefinedAction;
$"callee abstraction in synchronized call must be a left mover: {calleeActionDecl.Name}");
break;
}
else
if (calleeActionDecl == highestRefinedActionDecl)
{
actionDeclRef = null;
break;
}
calleeRefinedAction = calleeActionDecl.RefinedAction;
}
}
else if (isSkipped)
{
if (highestRefinedActionDecl.LayerRange.UpperLayer != callerDecl.Layer)
{
tc.Error(this, $"upper layer of action {highestRefinedActionDecl.Name} must be same as layer of caller");
}
else if (!highestRefinedActionDecl.IsSkippable())
{
tc.Error(this, $"action {highestRefinedActionDecl.Name} must be skippable");
}
}
}
Expand All @@ -357,41 +383,23 @@ void CheckModifies(IEnumerable<Variable> modifiedVars)
{
tc.Error(this, "caller must not be a mover procedure");
}
else if (IsAsync && isSynchronized)
{
tc.Error(this, "layer of callee in synchronized call must be less than layer of caller");
}
}

if (!IsAsync) {
var calleeRefinedAction = calleeDecl.RefinedAction;
while (calleeRefinedAction != null) {
var calleeActionDecl = calleeRefinedAction.ActionDecl;
if (calleeActionDecl.LayerRange.UpperLayer >= callerDecl.Layer) {
break;
}
calleeRefinedAction = calleeActionDecl.RefinedAction;
if (calleeRefinedAction != null && calleeRefinedAction.HasAttribute(CivlAttributes.IS_RIGHT)) {
tc.Error(this, "this must be an async call");
}
}
}
else if (!isSynchronized)
{
if (callerDecl.HasMoverType)
{
tc.Error(this, "caller must not be a mover procedure");
}
else if (calleeDecl.RefinedAction != null)
else if (IsAsync && calleeDecl.RefinedAction != null)
{
var highestRefinedAction = calleeDecl.RefinedActionAtLayer(callerDecl.Layer + 1);
if (highestRefinedAction == null)
if (isSynchronized)
{
tc.Error(this, $"called action is not available at layer {callerDecl.Layer + 1}");
tc.Error(this, "layer of callee in synchronized call must be less than layer of caller");
}
else if (!highestRefinedAction.MaybePendingAsync)
else
{
tc.Error(this, $"action {highestRefinedAction.Name} refined by callee must be eligible to be a pending async");
var highestRefinedAction = calleeDecl.RefinedActionAtLayer(callerDecl.Layer + 1);
if (highestRefinedAction == null)
{
tc.Error(this, $"called action is not available at layer {callerDecl.Layer + 1}");
}
else if (!highestRefinedAction.MaybePendingAsync)
{
tc.Error(this, $"action {highestRefinedAction.Name} refined by callee must be eligible to be a pending async");
}
}
}
}
Expand Down
2 changes: 1 addition & 1 deletion Source/Core/CivlAttributes.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -86,7 +86,7 @@ public static class CivlAttributes
public const string HIDE = "hide";
public const string PENDING_ASYNC = "pending_async";
public const string SYNC = "sync";

public const string SKIP = "skip";
public const string IS_RIGHT = "IS_right";
public const string IS_LEFT = "IS_left";

Expand Down
26 changes: 26 additions & 0 deletions Test/civl/regression-tests/refinement3.bpl
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,26 @@
// RUN: %parallel-boogie "%s" > "%t"
// RUN: %diff "%s.expect" "%t"

yield procedure {:layer 1} Good()
{
async call {:skip} P_A();
}

atomic action {:layer 1} A()
asserts true;
{}

yield procedure {:layer 0} P_A();
refines A;

yield procedure {:layer 1} Bad()
{
async call {:skip} P_B();
}

atomic action {:layer 1} B()
asserts false;
{}

yield procedure {:layer 0} P_B();
refines B;
5 changes: 5 additions & 0 deletions Test/civl/regression-tests/refinement3.bpl.expect
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
refinement3.bpl(22,1): Error: this gate of B could not be proved
Execution trace:
refinement3.bpl(18,11): anon0

Boogie program verifier finished with 3 verified, 1 error

0 comments on commit b5ea010

Please sign in to comment.