Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[Civl] Consolidation of pure procedures and actions #815

Merged
merged 7 commits into from
Nov 25, 2023
Merged

[Civl] Consolidation of pure procedures and actions #815

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
7 commits
Select commit Hold shift + click to select a range
dfb7293
added Copy procedure and replaced various snapshots with calls to Copy
shazqadeer Nov 21, 2023
d5b8df8
more snapshots eliminated
shazqadeer Nov 21, 2023
c22aa31
unified typing of pure procedures and primitives (incomplete)
shazqadeer Nov 23, 2023
58ed7f2
made mutable inout parameters of primitives consistently positioned
shazqadeer Nov 23, 2023
354eb92
fixed type checking
shazqadeer Nov 23, 2023
689c45d
fixed paxos
shazqadeer Nov 23, 2023
493721e
added pure actions in full
shazqadeer Nov 24, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 2 additions & 2 deletions Source/Concurrency/CivlCoreTypes.cs
View file
Open in desktop
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
Open in desktop
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
Open in desktop
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
Open in desktop
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
Open in desktop
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
Open in desktop
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
Open in desktop
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
Open in desktop
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
Loading