Skip to content

Commit

Permalink
[Civl] Consolidation of pure procedures and actions (#815)
Browse files Browse the repository at this point in the history
  • Loading branch information
@shazqadeer
shazqadeer authored Nov 25, 2023
1 parent b4c85a4 commit 25ae9d9
Show file tree
Hide file tree
Showing 60 changed files with 860 additions and 1,066 deletions.
4 changes: 2 additions & 2 deletions Source/Concurrency/CivlCoreTypes.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -186,8 +186,8 @@ private Function ComputeInputOutputRelation(CivlTypeChecker civlTypeChecker, Imp
var existsVars = foroldMap.Values
.Concat(alwaysMap.Keys.Where(key => key is GlobalVariable).Select(key => alwaysMap[key]))
.OfType<IdentifierExpr>().Select(ie => ie.Decl).ToList();
inputOutputRelation.Body =
ExprHelper.ExistsExpr(existsVars, Expr.And(gateExprs.Append(transitionRelationExpr)));
var expr = Expr.And(gateExprs.Append(transitionRelationExpr));
inputOutputRelation.Body = existsVars.Any() ? ExprHelper.ExistsExpr(existsVars, expr) : expr;
CivlUtil.ResolveAndTypecheck(civlTypeChecker.Options, inputOutputRelation.Body);
return inputOutputRelation;
}
Expand Down
13 changes: 2 additions & 11 deletions Source/Concurrency/CivlTypeChecker.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -16,7 +16,6 @@ public class CivlTypeChecker
private Dictionary<ActionDecl, Action> actionDeclToAction;
private List<Sequentialization> sequentializations;
private Dictionary<Implementation, Dictionary<CtorType, Variable>> implToPendingAsyncCollectors;
private HashSet<ActionDecl> linkActionDecls;
private string namePrefix;

public CivlTypeChecker(ConcurrencyOptions options, Program program)
Expand All @@ -33,7 +32,6 @@ public CivlTypeChecker(ConcurrencyOptions options, Program program)
this.actionDeclToAction = new Dictionary<ActionDecl, Action>();
this.sequentializations = new List<Sequentialization>();
this.implToPendingAsyncCollectors = new Dictionary<Implementation, Dictionary<CtorType, Variable>>();
this.linkActionDecls = new HashSet<ActionDecl>();

IEnumerable<string> declNames = program.TopLevelDeclarations.OfType<NamedDeclaration>().Select(x => x.Name);
IEnumerable<string> localVarNames = VariableNameCollector.Collect(program);
Expand All @@ -49,8 +47,8 @@ public CivlTypeChecker(ConcurrencyOptions options, Program program)
}
}

SkipActionDecl = new ActionDecl(Token.NoToken, AddNamePrefix("Skip"), MoverType.Both,
new List<Variable>(), new List<Variable>(), new List<ActionDeclRef>(), null, null, new List<ElimDecl>(),
SkipActionDecl = new ActionDecl(Token.NoToken, AddNamePrefix("Skip"), MoverType.Both, new List<Variable>(),
new List<Variable>(), true, new List<ActionDeclRef>(), null, null, new List<ElimDecl>(),
new List<IdentifierExpr>(), null, null);
var skipImplementation = DeclHelper.Implementation(
SkipActionDecl,
Expand Down Expand Up @@ -294,10 +292,6 @@ private void TypeCheckYieldingProcedures()
}
}
}
impl.Blocks.ForEach(block =>
{
block.Cmds.OfType<CallCmd>().Select(callCmd => callCmd.Proc).OfType<ActionDecl>().ForEach(actionDecl => linkActionDecls.Add(actionDecl));
});
}
}

Expand Down Expand Up @@ -454,9 +448,6 @@ private void MatchFormals(List<Variable> formals1, List<Variable> formals2, stri
#region Public access methods

public IEnumerable<Variable> GlobalVariables => program.GlobalVariables;

public IEnumerable<Action> LinkActions =>
actionDeclToAction.Values.Where(action => linkActionDecls.Contains(action.ActionDecl));

public IEnumerable<Action> MoverActions => actionDeclToAction.Keys
.Where(actionDecl => actionDecl.HasMoverType).Select(actionDecl => actionDeclToAction[actionDecl]);
Expand Down
6 changes: 3 additions & 3 deletions Source/Concurrency/LinearDomainCollector.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -138,7 +138,7 @@ private bool ContainsPermissionType(Type type)
visitedTypes.Add(type);
if (type is CtorType ctorType && ctorType.Decl is DatatypeTypeCtorDecl datatypeTypeCtorDecl)
{
var originalDecl = program.monomorphizer.GetOriginalDecl(datatypeTypeCtorDecl);
var originalDecl = Monomorphizer.GetOriginalDecl(datatypeTypeCtorDecl);
var originalDeclName = originalDecl.Name;
if (originalDeclName == "Lheap" || originalDeclName == "Lset" || originalDeclName == "Lval")
{
Expand Down Expand Up @@ -174,7 +174,7 @@ private bool ContainsPermissionType(Type type)
private Type GetPermissionType(Type type)
{
var typeCtorDecl = type.AsCtor.Decl;
var originalTypeCtorDecl = program.monomorphizer.GetOriginalDecl(typeCtorDecl);
var originalTypeCtorDecl = Monomorphizer.GetOriginalDecl(typeCtorDecl);
var actualTypeParams = program.monomorphizer.GetTypeInstantiation(typeCtorDecl);
return
originalTypeCtorDecl.Name == "Lheap"
Expand All @@ -189,7 +189,7 @@ private Dictionary<Type, LinearDomain> MakeLinearDomains()
foreach (var type in permissionTypes)
{
var typeCtorDecl = type.AsCtor.Decl;
var originalTypeCtorDecl = program.monomorphizer.GetOriginalDecl(typeCtorDecl);
var originalTypeCtorDecl = Monomorphizer.GetOriginalDecl(typeCtorDecl);
var actualTypeParams = program.monomorphizer.GetTypeInstantiation(typeCtorDecl);
var permissionType = GetPermissionType(type);
if (!permissionTypeToCollectors.ContainsKey(permissionType))
Expand Down
46 changes: 23 additions & 23 deletions Source/Concurrency/LinearRewriter.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -190,8 +190,8 @@ private List<Cmd> RewriteLheapSplit(CallCmd callCmd)
out Function lsetConstructor, out Function lvalConstructor);

var cmdSeq = new List<Cmd>();
var k = callCmd.Ins[0];
var path = callCmd.Ins[1];
var path = callCmd.Ins[0];
var k = callCmd.Ins[1];
var l = callCmd.Outs[0].Decl;

var mapImpFunc = MapImp(refType);
Expand Down Expand Up @@ -223,16 +223,16 @@ private List<Cmd> RewriteLheapTransfer(CallCmd callCmd)
out Function lsetConstructor, out Function lvalConstructor);

var cmdSeq = new List<Cmd>();
var path1 = callCmd.Ins[0];
var path2 = callCmd.Ins[1];
var path = callCmd.Ins[0];
var path1 = callCmd.Ins[1];

var mapOrFunc = MapOr(refType);
var mapIteFunc = MapIte(refType, type);
cmdSeq.Add(CmdHelper.AssignCmd(
CmdHelper.ExprToAssignLhs(path2),
CmdHelper.ExprToAssignLhs(path),
ExprHelper.FunctionCall(lheapConstructor,
ExprHelper.FunctionCall(mapOrFunc, Dom(path2), Dom(path1)),
ExprHelper.FunctionCall(mapIteFunc, Dom(path2), Val(path2), Val(path1)))));
ExprHelper.FunctionCall(mapOrFunc, Dom(path), Dom(path1)),
ExprHelper.FunctionCall(mapIteFunc, Dom(path), Val(path), Val(path1)))));

ResolveAndTypecheck(options, cmdSeq);
return cmdSeq;
Expand Down Expand Up @@ -286,7 +286,7 @@ private List<Cmd> CreateAccessAsserts(Expr expr, IToken tok, string msg)
if (mapExpr is NAryExpr lheapValExpr &&
lheapValExpr.Fun is FieldAccess &&
lheapValExpr.Args[0].Type is CtorType ctorType &&
monomorphizer.GetOriginalDecl(ctorType.Decl).Name == "Lheap")
Monomorphizer.GetOriginalDecl(ctorType.Decl).Name == "Lheap")
{
var cmdSeq = CreateAccessAsserts(lheapValExpr.Args[0], tok, msg);
var lheapContainsFunc = LheapContains(nAryExpr.Type);
Expand Down Expand Up @@ -371,9 +371,9 @@ private List<Cmd> RewriteLsetSplit(CallCmd callCmd)
out Function lsetConstructor, out Function lvalConstructor);

var cmdSeq = new List<Cmd>();
var k = callCmd.Ins[0];
var path = callCmd.Ins[1];
var path = callCmd.Ins[0];
var k = callCmd.Ins[1];

var mapConstFunc = MapConst(type, Type.Bool);
var mapImpFunc = MapImp(type);
cmdSeq.Add(AssertCmd(callCmd.tok,
Expand All @@ -394,13 +394,13 @@ private List<Cmd> RewriteLsetTransfer(CallCmd callCmd)
out Function lsetConstructor, out Function lvalConstructor);

var cmdSeq = new List<Cmd>();
var path1 = callCmd.Ins[0];
var path2 = callCmd.Ins[1];
var path = callCmd.Ins[0];
var path1 = callCmd.Ins[1];

var mapOrFunc = MapOr(type);
cmdSeq.Add(CmdHelper.AssignCmd(
CmdHelper.ExprToAssignLhs(path2),
ExprHelper.FunctionCall(lsetConstructor, ExprHelper.FunctionCall(mapOrFunc, Dom(path2), Dom(path1)))));
CmdHelper.ExprToAssignLhs(path),
ExprHelper.FunctionCall(lsetConstructor, ExprHelper.FunctionCall(mapOrFunc, Dom(path), Dom(path1)))));

ResolveAndTypecheck(options, cmdSeq);
return cmdSeq;
Expand All @@ -412,9 +412,9 @@ private List<Cmd> RewriteLvalSplit(CallCmd callCmd)
out Function lsetConstructor, out Function lvalConstructor);

var cmdSeq = new List<Cmd>();
var k = callCmd.Ins[0];
var path = callCmd.Ins[1];
var path = callCmd.Ins[0];
var k = callCmd.Ins[1];

var lsetContainsFunc = LsetContains(type);
cmdSeq.Add(AssertCmd(callCmd.tok, ExprHelper.FunctionCall(lsetContainsFunc, path, Val(k)), "Lval_Split failed"));

Expand All @@ -434,15 +434,15 @@ private List<Cmd> RewriteLvalTransfer(CallCmd callCmd)
out Function lsetConstructor, out Function lvalConstructor);

var cmdSeq = new List<Cmd>();
var l = callCmd.Ins[0];
var path2 = callCmd.Ins[1];

var path = callCmd.Ins[0];
var k = callCmd.Ins[1];
var mapOneFunc = MapOne(type);
var mapOrFunc = MapOr(type);
cmdSeq.Add(CmdHelper.AssignCmd(
CmdHelper.ExprToAssignLhs(path2),
CmdHelper.ExprToAssignLhs(path),
ExprHelper.FunctionCall(lsetConstructor,
ExprHelper.FunctionCall(mapOrFunc, Dom(path2), ExprHelper.FunctionCall(mapOneFunc, Val(l))))));
ExprHelper.FunctionCall(mapOrFunc, Dom(path), ExprHelper.FunctionCall(mapOneFunc, Val(k))))));

ResolveAndTypecheck(options, cmdSeq);
return cmdSeq;
Expand Down
89 changes: 19 additions & 70 deletions Source/Concurrency/LinearTypeChecker.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -280,7 +280,7 @@ private HashSet<Variable> PropagateAvailableLinearVarsAcrossBlock(Block b)
continue;
}
var ie = IsPrimitive(callCmd.Proc) && paramKind == LinearKind.LINEAR
? ExtractRootFromAccessPathExpr(callCmd.Ins[i])
? CivlPrimitives.ExtractRootFromAccessPathExpr(callCmd.Ins[i])
: callCmd.Ins[i] as IdentifierExpr;
if (start.Contains(ie.Decl))
{
Expand Down Expand Up @@ -393,69 +393,6 @@ private bool SkipCheck(Variable v)
return enclosingProc is ActionDecl || enclosingProc.IsPure;
}

private IdentifierExpr ExtractRootFromAccessPathExpr(Expr expr)
{
if (expr is IdentifierExpr identifierExpr)
{
return identifierExpr;
}
if (expr is NAryExpr nAryExpr)
{
if (nAryExpr.Fun is FieldAccess)
{
return ExtractRootFromAccessPathExpr(nAryExpr.Args[0]);
}
if (nAryExpr.Fun is MapSelect)
{
var mapExpr = nAryExpr.Args[0];
if (mapExpr is NAryExpr lheapValExpr &&
lheapValExpr.Fun is FieldAccess &&
lheapValExpr.Args[0].Type is CtorType ctorType &&
program.monomorphizer.GetOriginalDecl(ctorType.Decl).Name == "Lheap")
{
return ExtractRootFromAccessPathExpr(lheapValExpr.Args[0]);
}
return ExtractRootFromAccessPathExpr(nAryExpr.Args[0]);
}
}
return null;
}

private IdentifierExpr ModifiedArgument(CallCmd callCmd)
{
switch (Monomorphizer.GetOriginalDecl(callCmd.Proc).Name)
{
case "Ref_Alloc":
return null;
case "Lheap_Empty":
return null;
case "Lheap_Split":
return ExtractRootFromAccessPathExpr(callCmd.Ins[1]);
case "Lheap_Transfer":
return ExtractRootFromAccessPathExpr(callCmd.Ins[1]);
case "Lheap_Read":
return null;
case "Lheap_Write":
return ExtractRootFromAccessPathExpr(callCmd.Ins[0]);
case "Lheap_Alloc":
return ExtractRootFromAccessPathExpr(callCmd.Ins[0]);
case "Lheap_Remove":
return ExtractRootFromAccessPathExpr(callCmd.Ins[0]);
case "Lset_Empty":
return null;
case "Lset_Split":
return ExtractRootFromAccessPathExpr(callCmd.Ins[1]);
case "Lset_Transfer":
return ExtractRootFromAccessPathExpr(callCmd.Ins[1]);
case "Lval_Split":
return ExtractRootFromAccessPathExpr(callCmd.Ins[1]);
case "Lval_Transfer":
return ExtractRootFromAccessPathExpr(callCmd.Ins[1]);
default:
throw new cce.UnreachableException();
}
}

public override Cmd VisitAssignCmd(AssignCmd node)
{
HashSet<Variable> rhsVars = new HashSet<Variable>();
Expand Down Expand Up @@ -606,7 +543,8 @@ public int CheckLinearParameters(CallCmd callCmd, HashSet<Variable> availableLin
public override Cmd VisitCallCmd(CallCmd node)
{
var isPrimitive = IsPrimitive(node.Proc);
HashSet<Variable> inVars = new HashSet<Variable>();
var inVars = new HashSet<Variable>();
var globalInVars = new HashSet<Variable>();
for (int i = 0; i < node.Proc.InParams.Count; i++)
{
var formal = node.Proc.InParams[i];
Expand All @@ -616,7 +554,7 @@ public override Cmd VisitCallCmd(CallCmd node)
continue;
}
var isLinearParamInPrimitiveCall = isPrimitive && formalKind == LinearKind.LINEAR;
var actual = isLinearParamInPrimitiveCall ? ExtractRootFromAccessPathExpr(node.Ins[i]) : node.Ins[i] as IdentifierExpr;
var actual = isLinearParamInPrimitiveCall ? CivlPrimitives.ExtractRootFromAccessPathExpr(node.Ins[i]) : node.Ins[i] as IdentifierExpr;
if (actual == null)
{
if (isLinearParamInPrimitiveCall)
Expand All @@ -640,7 +578,7 @@ public override Cmd VisitCallCmd(CallCmd node)
Error(node, $"The domains of parameter {formal} and argument {actual} must be the same");
continue;
}
if (actual.Decl is GlobalVariable && !IsPrimitive(node.Proc))
if (actual.Decl is GlobalVariable && !node.Proc.IsPure)
{
Error(node, $"Only local linear variable can be an argument to a procedure call: {actual}");
continue;
Expand All @@ -651,6 +589,10 @@ public override Cmd VisitCallCmd(CallCmd node)
continue;
}
inVars.Add(actual.Decl);
if (actual.Decl is GlobalVariable && actualKind == LinearKind.LINEAR_IN)
{
globalInVars.Add(actual.Decl);
}
}

for (int i = 0; i < node.Proc.OutParams.Count; i++)
Expand All @@ -674,9 +616,15 @@ public override Cmd VisitCallCmd(CallCmd node)
}
}

var globalOutVars = node.Outs.Select(ie => ie.Decl).ToHashSet();
globalInVars.Where(v => !globalOutVars.Contains(v)).ForEach(v =>
{
Error(node, $"Global variable passed as input to pure call but not received as output: {v}");
});

if (isPrimitive)
{
var modifiedArgument = ModifiedArgument(node)?.Decl;
var modifiedArgument = CivlPrimitives.ModifiedArgument(node)?.Decl;
if (modifiedArgument != null)
{
if (modifiedArgument is Formal formal && formal.InComing)
Expand All @@ -687,8 +635,9 @@ public override Cmd VisitCallCmd(CallCmd node)
enclosingProc is not YieldProcedureDecl &&
enclosingProc.Modifies.All(v => v.Decl != modifiedArgument))
{
var str = enclosingProc is ActionDecl ? "action's" : "procedure's";
Error(node,
$"Primitive assigns to a global variable that is not in the enclosing procedure's modifies clause: {modifiedArgument}");
$"Primitive assigns to a global variable that is not in the enclosing {str} modifies clause: {modifiedArgument}");
}
}
}
Expand Down Expand Up @@ -793,7 +742,7 @@ public IEnumerable<Expr> LheapWellFormedExpressions(IEnumerable<Variable> availa
return Enumerable.Empty<Expr>();
}
return availableVars.Where(v =>
v.TypedIdent.Type is CtorType ctorType && monomorphizer.GetOriginalDecl(ctorType.Decl).Name == "Lheap").Select(
v.TypedIdent.Type is CtorType ctorType && Monomorphizer.GetOriginalDecl(ctorType.Decl).Name == "Lheap").Select(
v =>
{
var ctorType = (CtorType)v.TypedIdent.Type;
Expand Down
2 changes: 1 addition & 1 deletion Source/Concurrency/LinearityChecker.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -15,7 +15,7 @@ private LinearityChecker(CivlTypeChecker civlTypeChecker)
public static void AddCheckers(CivlTypeChecker civlTypeChecker, List<Declaration> decls)
{
var linearityChecker = new LinearityChecker(civlTypeChecker);
foreach (var action in civlTypeChecker.MoverActions.Concat<Action>(civlTypeChecker.LinkActions))
foreach (var action in civlTypeChecker.MoverActions)
{
linearityChecker.AddChecker(action, decls);
}
Expand Down
5 changes: 0 additions & 5 deletions Source/Concurrency/MoverCheck.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -82,11 +82,6 @@ where action.LayerRange.Contains(sequentialization.Layer)
{
moverChecking.CreateCooperationChecker(action);
}

foreach (var action in civlTypeChecker.LinkActions)
{
moverChecking.CreateCooperationChecker(action);
}
}

private IEnumerable<Requires> DisjointnessAndWellFormedRequires(IEnumerable<Variable> paramVars, HashSet<Variable> frame)
Expand Down
6 changes: 3 additions & 3 deletions Source/Concurrency/YieldSufficiencyTypeChecker.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -16,7 +16,7 @@ public static class YieldSufficiencyTypeChecker
private const string L = "L"; // left mover action
private const string R = "R"; // right mover action
private const string N = "N"; // non mover action
private const string P = "P"; // private access (local variable, link action, pure procedure, ...)
private const string P = "P"; // private access (local variable, pure action, pure procedure, ...)
private const string M = "M"; // modification of global variables
private const string A = "A"; // async call

Expand Down Expand Up @@ -318,7 +318,7 @@ private static List<Tuple<Absy, string, Absy>> LabelsToLabeledEdges(Dictionary<T

private string CallCmdLabel(CallCmd callCmd)
{
if (callCmd.Proc is ActionDecl || LinearRewriter.IsPrimitive(callCmd.Proc) || callCmd.Proc.IsPure)
if (callCmd.Proc.IsPure)
{
return P;
}
Expand Down Expand Up @@ -387,7 +387,7 @@ public static string ModifiesGlobalLabel<T>(IEnumerable<T> modifiedGlobalVars)

private string CallCmdLabelAsync(CallCmd callCmd)
{
if (callCmd.Proc is ActionDecl || LinearRewriter.IsPrimitive(callCmd.Proc) || callCmd.Proc.IsPure)
if (callCmd.Proc.IsPure)
{
return P;
}
Expand Down
Loading

0 comments on commit 25ae9d9

Please sign in to comment.