Skip to content

Commit

Permalink
[Civl] Eliminated linearity checks in favor of local checks (#914)
Browse files Browse the repository at this point in the history
  • Loading branch information
@shazqadeer
shazqadeer authored Jul 22, 2024
1 parent 599970f commit 1b8d963
Show file tree
Hide file tree
Showing 46 changed files with 497 additions and 758 deletions.
45 changes: 31 additions & 14 deletions Source/Concurrency/CivlCoreTypes.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -49,7 +49,7 @@ public Action(CivlTypeChecker civlTypeChecker, ActionDecl actionDecl, Action ref
civlTypeChecker.program.AddTopLevelDeclaration(ChoiceDatatypeTypeCtorDecl);
DesugarSetChoice(civlTypeChecker, ImplWithChoice);
}
DropSetChoice(civlTypeChecker, Impl);
DropSetChoice(Impl);
}

ModifiedGlobalVars = new HashSet<Variable>(Impl.Proc.Modifies.Select(x => x.Decl));
Expand Down Expand Up @@ -176,19 +176,24 @@ private void AddGateSufficiencyCheckerAndHoistAsserts(CivlTypeChecker civlTypeCh
return;
}

var gateSubst = Substituter.SubstitutionFromDictionary(ActionDecl.InParams
.Zip(Impl.InParams)
.ToDictionary(x => x.Item1, x => (Expr)Expr.Ident(x.Item2)));

var checkerName = $"{Name}_GateSufficiencyChecker";
var checkerImpl = new Duplicator().VisitImplementation(ActionDecl.Impl);
var checkerImpl = new Duplicator().VisitImplementation(Impl);
checkerImpl.Name = checkerName;
checkerImpl.Attributes = null;
var requires = ActionDecl.Requires.Select(
requires => new Requires(requires.tok, requires.Free, Substituter.Apply(gateSubst, requires.Condition),
null, CivlAttributes.ApplySubstitutionToPoolHints(gateSubst, requires.Attributes))).ToList();
var proc = checkerImpl.Proc;
checkerImpl.Proc = new Procedure(proc.tok, checkerName, proc.TypeParameters, proc.InParams,
proc.OutParams, proc.IsPure, proc.Requires, proc.Modifies, proc.Ensures);
proc.OutParams, proc.IsPure, requires, proc.Modifies, new List<Ensures>());
gateSufficiencyCheckerDecls.AddRange(new Declaration[] { checkerImpl.Proc, checkerImpl });

HoistAsserts(Impl, civlTypeChecker.Options);
var gateSubst = Substituter.SubstitutionFromDictionary(ActionDecl.InParams
.Zip(Impl.InParams)
.ToDictionary(x => x.Item1, x => (Expr)Expr.Ident(x.Item2)));

Gate = ActionDecl.Requires.Select(
requires => new AssertCmd(requires.tok, Substituter.Apply(gateSubst, requires.Condition),
CivlAttributes.ApplySubstitutionToPoolHints(gateSubst, requires.Attributes))).ToList();
Expand Down Expand Up @@ -256,24 +261,36 @@ public static void DesugarCreateAsyncs(CivlTypeChecker civlTypeChecker, Implemen
if (cmd is CallCmd callCmd)
{
var originalProc = (Procedure)Monomorphizer.GetOriginalDecl(callCmd.Proc);
if (originalProc.Name == "create_async" || originalProc.Name == "create_asyncs" || originalProc.Name == "create_multi_asyncs")
if (callCmd.IsAsync)
{
var actionDecl = (ActionDecl)callCmd.Proc;
var pendingAsyncMultiset =
Expr.Store(
ExprHelper.FunctionCall(actionDecl.PendingAsyncConst, Expr.Literal(0)),
ExprHelper.FunctionCall(actionDecl.PendingAsyncCtor, callCmd.Ins),
Expr.Literal(1));
var pendingAsyncMultisetType = TypeHelper.MapType(actionDecl.PendingAsyncType, Type.Int);
var pendingAsyncCollector = impl.OutParams.Skip(actionDecl.OutParams.Count).First(v => v.TypedIdent.Type.Equals(pendingAsyncMultisetType));
var updateAssignCmd = CmdHelper.AssignCmd(pendingAsyncCollector,
ExprHelper.FunctionCall(actionDecl.PendingAsyncAdd, Expr.Ident(pendingAsyncCollector), pendingAsyncMultiset));
updateAssignCmd.Typecheck(tc);
newCmds.Add(updateAssignCmd);
continue;
}
else if (originalProc.Name == "create_asyncs" || originalProc.Name == "create_multi_asyncs")
{
var pendingAsyncType =
(CtorType)civlTypeChecker.program.monomorphizer.GetTypeInstantiation(callCmd.Proc)["T"];
var pendingAsync = pendingAsyncTypeToActionDecl[pendingAsyncType];
var pendingAsyncMultiset = originalProc.Name == "create_async"
? Expr.Store(ExprHelper.FunctionCall(pendingAsync.PendingAsyncConst, Expr.Literal(0)), callCmd.Ins[0],
Expr.Literal(1))
: originalProc.Name == "create_asyncs"
var pendingAsyncMultiset = originalProc.Name == "create_asyncs"
? ExprHelper.FunctionCall(pendingAsync.PendingAsyncIte, callCmd.Ins[0],
ExprHelper.FunctionCall(pendingAsync.PendingAsyncConst, Expr.Literal(1)),
ExprHelper.FunctionCall(pendingAsync.PendingAsyncConst, Expr.Literal(0)))
: callCmd.Ins[0];
var pendingAsyncMultisetType = TypeHelper.MapType(pendingAsyncType, Type.Int);
var pendingAsyncCollector = impl.OutParams.Skip(actionDecl.OutParams.Count).First(v => v.TypedIdent.Type.Equals(pendingAsyncMultisetType));
var updateAssignCmd = CmdHelper.AssignCmd(pendingAsyncCollector,
ExprHelper.FunctionCall(pendingAsync.PendingAsyncAdd, Expr.Ident(pendingAsyncCollector),
pendingAsyncMultiset));
ExprHelper.FunctionCall(pendingAsync.PendingAsyncAdd, Expr.Ident(pendingAsyncCollector), pendingAsyncMultiset));
updateAssignCmd.Typecheck(tc);
newCmds.Add(updateAssignCmd);
continue;
Expand All @@ -285,7 +302,7 @@ public static void DesugarCreateAsyncs(CivlTypeChecker civlTypeChecker, Implemen
});
}

private void DropSetChoice(CivlTypeChecker civlTypeChecker, Implementation impl)
private void DropSetChoice(Implementation impl)
{
impl.Blocks.ForEach(block =>
{
Expand Down
3 changes: 0 additions & 3 deletions Source/Concurrency/CivlRewriter.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -45,9 +45,6 @@ public static void Transform(ConcurrencyOptions options, CivlTypeChecker civlTyp
// Desugaring of yielding procedures
YieldingProcChecker.AddCheckers(civlTypeChecker, decls);

// Linear type checks
LinearityChecker.AddCheckers(civlTypeChecker, decls);

if (!options.TrustSequentialization)
{
Sequentialization.AddCheckers(civlTypeChecker, decls);
Expand Down
4 changes: 2 additions & 2 deletions Source/Concurrency/CivlTypeChecker.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -132,7 +132,7 @@ private HashSet<ActionDecl> TypeCheckActions()
{
foreach (var block in actionDecl.Impl.Blocks)
{
foreach (var callCmd in block.Cmds.OfType<CallCmd>())
foreach (var callCmd in block.Cmds.OfType<CallCmd>().Where(callCmd => !callCmd.IsAsync))
{
callGraph.AddEdge(actionDecl, callCmd.Proc);
}
Expand Down Expand Up @@ -220,7 +220,7 @@ private void CheckAsyncToSyncSafety(ActionDecl actionDecl, HashSet<string> refin
for (int i = block.Cmds.Count - 1; 0 <= i; i--)
{
var cmd = block.Cmds[i];
if (modifiedGlobals && cmd is CallCmd callCmd && callCmd.Proc.OriginalDeclWithFormals is { Name: "create_async" })
if (modifiedGlobals && cmd is CallCmd callCmd && callCmd.IsAsync)
{
var pendingAsyncType = (CtorType)program.monomorphizer.GetTypeInstantiation(callCmd.Proc)["T"];
if (!refinedActionCreateNames.Contains(pendingAsyncType.Decl.Name))
Expand Down
28 changes: 22 additions & 6 deletions Source/Concurrency/InductiveSequentialization.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -5,6 +5,24 @@

namespace Microsoft.Boogie
{
public class LinearityCheck
{
public LinearDomain domain;
public Expr assume;
public Expr assert;
public string message;
public string checkName;

public LinearityCheck(LinearDomain domain, Expr assume, Expr assert, string message, string checkName)
{
this.domain = domain;
this.assume = assume;
this.assert = assert;
this.message = message;
this.checkName = checkName;
}
}

public enum InductiveSequentializationRule
{
ISL,
Expand Down Expand Up @@ -292,16 +310,14 @@ private Implementation CreateInlinedImplementation()

private Cmd Transform(Dictionary<CtorType, Implementation> eliminatedPendingAsyncs, Cmd cmd, HashSet<Variable> modifies)
{
if (cmd is CallCmd callCmd && callCmd.Proc.OriginalDeclWithFormals is { Name: "create_async" })
if (cmd is CallCmd callCmd && callCmd.IsAsync)
{
var pendingAsyncType = (CtorType)civlTypeChecker.program.monomorphizer.GetTypeInstantiation(callCmd.Proc)["T"];
var datatypeTypeCtorDecl = (DatatypeTypeCtorDecl)pendingAsyncType.Decl;
var actionDecl = (ActionDecl)callCmd.Proc;
var pendingAsyncType = actionDecl.PendingAsyncType;
if (eliminatedPendingAsyncs.ContainsKey(pendingAsyncType))
{
var newCallee = eliminatedPendingAsyncs[pendingAsyncType].Proc;
var newIns = datatypeTypeCtorDecl.Constructors[0].InParams
.Select(x => (Expr)ExprHelper.FieldAccess(callCmd.Ins[0], x.Name)).ToList();
var newCallCmd = new CallCmd(callCmd.tok, newCallee.Name, newIns, new List<IdentifierExpr>())
var newCallCmd = new CallCmd(callCmd.tok, newCallee.Name, callCmd.Ins, new List<IdentifierExpr>())
{
Proc = newCallee
};
Expand Down
96 changes: 96 additions & 0 deletions Source/Concurrency/LinearRewriter.cs
View file
Original file line number Diff line number Diff line change
@@ -1,5 +1,6 @@
using System.Collections.Generic;
using System.Diagnostics.Contracts;
using System.Linq;

namespace Microsoft.Boogie;

Expand Down Expand Up @@ -41,6 +42,11 @@ private List<Cmd> RewriteCmdSeq(List<Cmd> cmdSeq)
{
newCmdSeq.AddRange(RewriteCallCmd(callCmd));
}
else if (Monomorphizer.GetOriginalDecl(callCmd.Proc).Name == "create_asyncs")
{
newCmdSeq.AddRange(PreconditionsForCreateAsyncs(callCmd));
newCmdSeq.Add(cmd);
}
else
{
newCmdSeq.Add(cmd);
Expand All @@ -54,6 +60,91 @@ private List<Cmd> RewriteCmdSeq(List<Cmd> cmdSeq)
return newCmdSeq;
}

private List<Cmd> PreconditionsForCreateAsyncs(CallCmd callCmd)
{
var cmds = new List<Cmd>();
var attr = QKeyValue.FindAttribute(callCmd.Attributes, x => x.Key == "linear");
if (attr == null)
{
return cmds;
}

var sources = attr.Params.OfType<Expr>();
var pendingAsyncType = civlTypeChecker.program.monomorphizer.GetTypeInstantiation(callCmd.Proc)["T"];
var actionDecl = civlTypeChecker.linearTypeChecker.GetActionDeclFromCreateAsyncs(callCmd);
var iter = Enumerable.Range(0, actionDecl.InParams.Count).Where(i => {
var inParam = actionDecl.InParams[i];
if (LinearTypeChecker.FindLinearKind(inParam) == LinearKind.ORDINARY)
{
return false;
}
if (inParam.TypedIdent.Type is not CtorType ctorType)
{
return false;
}
var originalTypeCtorDecl = Monomorphizer.GetOriginalDecl(ctorType.Decl);
return originalTypeCtorDecl.Name == "One" || originalTypeCtorDecl.Name == "Set";
});
var datatypeTypeCtorDecl = (DatatypeTypeCtorDecl) actionDecl.PendingAsyncType.Decl;
var constructor = datatypeTypeCtorDecl.Constructors[0];

var paVar = civlTypeChecker.BoundVariable("pa", actionDecl.PendingAsyncType);
var containsExpr = NAryExpr.Select(callCmd.Ins[0], Expr.Ident(paVar));
var containsCheckExprs = iter.Zip(sources).Select(kv => {
var i = kv.First;
var sourceExpr = kv.Second;
var inParam = actionDecl.InParams[i];
var ctorType = (CtorType)inParam.TypedIdent.Type;
var originalTypeCtorDecl = Monomorphizer.GetOriginalDecl(ctorType.Decl);
var instanceType = civlTypeChecker.program.monomorphizer.GetTypeInstantiation(ctorType.Decl)[0];
var fieldAccess = ExprHelper.FieldAccess(Expr.Ident(paVar), constructor.InParams[i].Name);
if (originalTypeCtorDecl.Name == "One")
{
fieldAccess = ExprHelper.FieldAccess(fieldAccess, "val");
return ExprHelper.FunctionCall(SetContains(instanceType), sourceExpr, fieldAccess);
}
else
{
return ExprHelper.FunctionCall(SetIsSubset(instanceType), fieldAccess, sourceExpr);
}
});
var containsCheckExpr = ExprHelper.ForallExpr(
new List<Variable>(){ paVar },
Expr.Imp(containsExpr, Expr.And(containsCheckExprs)));
cmds.Add(CmdHelper.AssertCmd(callCmd.tok, containsCheckExpr, "Contains check failed"));

var paVar1 = civlTypeChecker.BoundVariable("pa1", actionDecl.PendingAsyncType);
var paVar2 = civlTypeChecker.BoundVariable("pa2", actionDecl.PendingAsyncType);
var guardExprs = new List<Expr>() {
NAryExpr.Select(callCmd.Ins[0], Expr.Ident(paVar1)),
NAryExpr.Select(callCmd.Ins[0], Expr.Ident(paVar2)),
Expr.Neq(Expr.Ident(paVar1), Expr.Ident(paVar2))
};
var distinctCheckExprs = iter.Select(i => {
var inParam = actionDecl.InParams[i];
var ctorType = (CtorType)inParam.TypedIdent.Type;
var originalTypeCtorDecl = Monomorphizer.GetOriginalDecl(ctorType.Decl);
var instanceType = civlTypeChecker.program.monomorphizer.GetTypeInstantiation(ctorType.Decl)[0];
var fieldAccess1 = ExprHelper.FieldAccess(Expr.Ident(paVar1), constructor.InParams[i].Name);
var fieldAccess2 = ExprHelper.FieldAccess(Expr.Ident(paVar2), constructor.InParams[i].Name);
if (originalTypeCtorDecl.Name == "One")
{
return Expr.Neq(fieldAccess1, fieldAccess2);
}
else
{
return ExprHelper.FunctionCall(SetIsDisjoint(instanceType), fieldAccess1, fieldAccess2);
}
});
var distinctCheckExpr = ExprHelper.ForallExpr(
new List<Variable>(){ paVar1, paVar2 },
Expr.Imp(Expr.And(guardExprs), Expr.And(distinctCheckExprs)));
cmds.Add(CmdHelper.AssertCmd(callCmd.tok, distinctCheckExpr, "Distinct check failed"));

ResolveAndTypecheck(options, cmds);
return cmds;
}

public List<Cmd> RewriteCallCmd(CallCmd callCmd)
{
switch (Monomorphizer.GetOriginalDecl(callCmd.Proc).Name)
Expand Down Expand Up @@ -122,6 +213,11 @@ private Function SetIsSubset(Type type)
return monomorphizer.InstantiateFunction("Set_IsSubset", new Dictionary<string, Type>() { { "T", type } });
}

private Function SetIsDisjoint(Type type)
{
return monomorphizer.InstantiateFunction("Set_IsDisjoint",new Dictionary<string, Type>() { { "T", type } });
}

private Function SetAdd(Type type)
{
return monomorphizer.InstantiateFunction("Set_Add",new Dictionary<string, Type>() { { "T", type } });
Expand Down
Loading

0 comments on commit 1b8d963

Please sign in to comment.