Skip to content

Commit

Permalink
[Civl] Removed ElimDecl (#873)
Browse files Browse the repository at this point in the history 
This PR removes ElimDecl from Civl since its functionality is now
covered by action preconditions.

Co-authored-by: Shaz Qadeer <[email protected]>
  • Loading branch information
@shazqadeer
shazqadeer and Shaz Qadeer authored Apr 22, 2024
1 parent df44c91 commit 4b8a095
Show file tree
Hide file tree
Showing 10 changed files with 478 additions and 656 deletions.
7 changes: 1 addition & 6 deletions Source/Concurrency/CivlTypeChecker.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -52,7 +52,7 @@ public CivlTypeChecker(ConcurrencyOptions options, Program program)
}

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<Requires>(), new List<CallCmd>(),
new List<Variable>(), true, new List<ActionDeclRef>(), null, null, new List<Requires>(), new List<CallCmd>(),
new List<IdentifierExpr>(), null, null);
var skipImplementation = DeclHelper.Implementation(
SkipActionDecl,
Expand Down Expand Up @@ -146,11 +146,6 @@ private HashSet<ActionDecl> TypeCheckActions()
{
SignatureMatcher.CheckSequentializationSignature(actionDecl, actionDecl.RefinedAction.ActionDecl,
checkingContext);
foreach (var elimDecl in actionDecl.Eliminates)
{
SignatureMatcher.CheckSequentializationSignature(elimDecl.Target.ActionDecl, elimDecl.Abstraction.ActionDecl,
checkingContext);
}
if (actionDecl.InvariantAction != null)
{
SignatureMatcher.CheckSequentializationSignature(actionDecl, actionDecl.InvariantAction.ActionDecl,
Expand Down
84 changes: 27 additions & 57 deletions Source/Concurrency/InductiveSequentialization.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -9,20 +9,16 @@ public abstract class Sequentialization
{
protected CivlTypeChecker civlTypeChecker;
protected Action targetAction;
protected Dictionary<Action, Action> elim;
protected HashSet<Action> eliminatedActions;

protected Sequentialization(CivlTypeChecker civlTypeChecker, Action targetAction)
{
this.civlTypeChecker = civlTypeChecker;
this.targetAction = targetAction;
this.elim = new Dictionary<Action, Action>(targetAction.ActionDecl.EliminationMap().Select(x =>
KeyValuePair.Create(civlTypeChecker.Action(x.Key), civlTypeChecker.Action(x.Value))));
this.eliminatedActions = new HashSet<Action>(targetAction.ActionDecl.EliminatedActionDecls().Select(x => civlTypeChecker.Action(x)));
}

public IEnumerable<Action> Abstractions => elim.Values;

private IEnumerable<Tuple<Action, Action>> AbstractionChecks =>
elim.Where(kv => kv.Key != kv.Value).Select(kv => Tuple.Create(kv.Key, kv.Value));
public IEnumerable<Action> EliminatedActions => eliminatedActions;

public int Layer => targetAction.LayerRange.UpperLayer;

Expand Down Expand Up @@ -63,29 +59,6 @@ public static void AddCheckers(CivlTypeChecker civlTypeChecker, List<Declaration
{
decls.AddRange(x.GenerateCheckers());
}
foreach (var tuple in civlTypeChecker.Sequentializations.SelectMany(x => x.AbstractionChecks).Distinct())
{
decls.AddRange(GenerateAbstractionChecker(civlTypeChecker, tuple.Item1, tuple.Item2));
}
}

private static List<Declaration> GenerateAbstractionChecker(CivlTypeChecker civlTypeChecker, Action action, Action abs)
{
var requires = abs.Gate.Select(g => new Requires(false, g.Expr)).ToList();
// The type checker ensures that the modified set of abs is a subset of the modified set of action.
var frame = new HashSet<Variable>(action.ModifiedGlobalVars);

var subst = action.GetSubstitution(abs);
var cmds = action.GetGateAsserts(subst, $"Abstraction {abs.Name} fails gate of {action.Name}").ToList<Cmd>();
cmds.Add(CmdHelper.CallCmd(action.Impl.Proc, abs.Impl.InParams, abs.Impl.OutParams));
cmds.Add(CmdHelper.AssertCmd(abs.tok, abs.GetTransitionRelation(civlTypeChecker, frame),
$"Abstraction {abs.Name} does not summarize {action.Name}"));

var blocks = new List<Block> { BlockHelper.Block("init", cmds) };
var proc = DeclHelper.Procedure(civlTypeChecker.AddNamePrefix($"AbstractionCheck_{action.Name}_{abs.Name}"),
abs.Impl.InParams, abs.Impl.OutParams, requires, action.Impl.Proc.Modifies, new List<Ensures>());
var impl = DeclHelper.Implementation(proc, proc.InParams, proc.OutParams, new List<Variable>(), blocks);
return new List<Declaration>(new Declaration[] { proc, impl });
}
}

Expand Down Expand Up @@ -128,19 +101,18 @@ protected override List<Declaration> GenerateCheckers()

private Implementation CreateInlinedImplementation()
{
var eliminatedActionDecls = targetAction.ActionDecl.EliminationMap();
var eliminatedActions = eliminatedActionDecls.Keys.ToHashSet();
var eliminatedActionDecls = targetAction.ActionDecl.EliminatedActionDecls();
var graph = new Graph<ActionDecl>();
eliminatedActions.ForEach(actionDecl =>
eliminatedActionDecls.ForEach(actionDecl =>
{
graph.AddSource(actionDecl);
CollectionExtensions.ForEach(actionDecl.CreateActionDecls.Intersect(eliminatedActions), x => graph.AddEdge(x, actionDecl));
CollectionExtensions.ForEach(actionDecl.CreateActionDecls.Intersect(eliminatedActionDecls), x => graph.AddEdge(x, actionDecl));
});
var eliminatedPendingAsyncs = new Dictionary<CtorType, Implementation>();
var decls = new List<Declaration>();
graph.TopologicalSort().ForEach(actionDecl =>
{
var impl = Action.CreateDuplicateImplementation(eliminatedActionDecls[actionDecl].Impl,
var impl = Action.CreateDuplicateImplementation(actionDecl.Impl,
$"{actionDecl.Name}_RefinementCheck");
eliminatedPendingAsyncs[actionDecl.PendingAsyncType] = impl;
decls.Add(impl);
Expand Down Expand Up @@ -291,41 +263,40 @@ private List<Declaration> GenerateStepChecker(Action pendingAsync)
Expr.Literal(0))));
cmds.Add(RemoveChoice(pendingAsyncType));

Action abs = elim[pendingAsync];
List<Expr> inputExprs = new List<Expr>();
for (int i = 0; i < abs.Impl.InParams.Count; i++)
for (int i = 0; i < pendingAsync.Impl.InParams.Count; i++)
{
inputExprs.Add(ExprHelper.FieldAccess(Choice(pendingAsyncType), pendingAsyncCtor.InParams[i].Name));
}
cmds.AddRange(abs.GetGateAsserts(Substituter.SubstitutionFromDictionary(abs.Impl.InParams.Zip(inputExprs).ToDictionary(x => x.Item1, x => x.Item2)),
$"Gate of {abs.Name} fails in IS induction step for invariant {invariantAction.Name}"));
cmds.AddRange(Preconditions(abs, Substituter.SubstitutionFromDictionary(abs.ActionDecl.InParams.Zip(inputExprs).ToDictionary(x => x.Item1, x => x.Item2))));
cmds.AddRange(pendingAsync.GetGateAsserts(Substituter.SubstitutionFromDictionary(pendingAsync.Impl.InParams.Zip(inputExprs).ToDictionary(x => x.Item1, x => x.Item2)),
$"Gate of {pendingAsync.Name} fails in IS induction step for invariant {invariantAction.Name}"));
cmds.AddRange(Preconditions(pendingAsync, Substituter.SubstitutionFromDictionary(pendingAsync.ActionDecl.InParams.Zip(inputExprs).ToDictionary(x => x.Item1, x => x.Item2))));

List<IdentifierExpr> outputExprs = new List<IdentifierExpr>();
if (abs.HasPendingAsyncs)
if (pendingAsync.HasPendingAsyncs)
{
abs.PendingAsyncs.ForEach(decl =>
pendingAsync.PendingAsyncs.ForEach(decl =>
{
var ie = NewPAs(decl.PendingAsyncType);
locals.Add(ie.Decl);
outputExprs.Add(ie);
});
}
cmds.Add(CmdHelper.CallCmd(abs.Impl.Proc, inputExprs, outputExprs));
if (abs.HasPendingAsyncs)
cmds.Add(CmdHelper.CallCmd(pendingAsync.Impl.Proc, inputExprs, outputExprs));
if (pendingAsync.HasPendingAsyncs)
{
var lhss = abs.PendingAsyncs.Select(decl => new SimpleAssignLhs(Token.NoToken, PAs(decl.PendingAsyncType)))
var lhss = pendingAsync.PendingAsyncs.Select(decl => new SimpleAssignLhs(Token.NoToken, PAs(decl.PendingAsyncType)))
.ToList<AssignLhs>();
var rhss = abs.PendingAsyncs.Select(decl => ExprHelper.FunctionCall(decl.PendingAsyncAdd,
var rhss = pendingAsync.PendingAsyncs.Select(decl => ExprHelper.FunctionCall(decl.PendingAsyncAdd,
PAs(decl.PendingAsyncType), NewPAs(decl.PendingAsyncType))).ToList<Expr>();
cmds.Add(new AssignCmd(Token.NoToken, lhss, rhss));
}

var frame = new HashSet<Variable>(invariantAction.ModifiedGlobalVars);
cmds.Add(GetCheck(invariantAction.tok, invariantAction.GetTransitionRelation(civlTypeChecker, frame),
$"IS step of {invariantAction.Name} with {abs.Name} failed"));
$"IS step of {invariantAction.Name} with {pendingAsync.Name} failed"));

return GetCheckerTuple($"IS_step_{invariantAction.Name}_{abs.Name}", requires,
return GetCheckerTuple($"IS_step_{invariantAction.Name}_{pendingAsync.Name}", requires,
invariantAction.ImplWithChoice.InParams, invariantAction.ImplWithChoice.OutParams, locals, cmds);
}

Expand Down Expand Up @@ -374,7 +345,7 @@ public override IEnumerable<Expr> GenerateMoverCheckAssumptions(Action action, L

private Expr ActionExpr(Action action, List<Variable> actionArgs, Substitution invariantFormalSubst)
{
if (!elim.ContainsKey(action))
if (!eliminatedActions.Contains(action))
{
return Expr.True;
}
Expand Down Expand Up @@ -418,17 +389,16 @@ private Expr ActionExpr(Action action, List<Variable> actionArgs, Substitution i

private Expr LeftMoverExpr(Action leftMover, List<Variable> leftMoverArgs, Substitution invariantFormalSubst)
{
var asyncLeftMover = elim.First(x => x.Value == leftMover).Key;
var leftMoverPendingAsyncCtor = asyncLeftMover.ActionDecl.PendingAsyncCtor;
var leftMoverPendingAsyncCtor = leftMover.ActionDecl.PendingAsyncCtor;
var leftMoverPA =
ExprHelper.FunctionCall(leftMoverPendingAsyncCtor, leftMoverArgs.Select(v => Expr.Ident(v)).ToArray());
var leftMoverExpr = Expr.And(new[]
{
ChoiceTest(asyncLeftMover.ActionDecl.PendingAsyncType),
ChoiceTest(leftMover.ActionDecl.PendingAsyncType),
Expr.Gt(
Expr.Select(PAs(asyncLeftMover.ActionDecl.PendingAsyncType),
Choice(asyncLeftMover.ActionDecl.PendingAsyncType)), Expr.Literal(0)),
Expr.Eq(Choice(asyncLeftMover.ActionDecl.PendingAsyncType), leftMoverPA)
Expr.Select(PAs(leftMover.ActionDecl.PendingAsyncType),
Choice(leftMover.ActionDecl.PendingAsyncType)), Expr.Literal(0)),
Expr.Eq(Choice(leftMover.ActionDecl.PendingAsyncType), leftMoverPA)
});
leftMoverExpr = Substituter.Apply(invariantFormalSubst, leftMoverExpr);
return leftMoverExpr;
Expand Down Expand Up @@ -483,7 +453,7 @@ private Expr NoPendingAsyncs
{
get
{
var expr = Expr.And(elim.Keys.Select(action => Expr.Eq(PAs(action.ActionDecl.PendingAsyncType),
var expr = Expr.And(eliminatedActions.Select(action => Expr.Eq(PAs(action.ActionDecl.PendingAsyncType),
ExprHelper.FunctionCall(action.ActionDecl.PendingAsyncConst, Expr.Literal(0)))));
expr.Typecheck(new TypecheckingContext(null, civlTypeChecker.Options));
return expr;
Expand All @@ -501,7 +471,7 @@ protected override List<Declaration> GenerateCheckers()
var decls = new List<Declaration>();
decls.AddRange(GenerateBaseCaseChecker());
decls.AddRange(GenerateConclusionChecker());
foreach (var elim in elim.Keys)
foreach (var elim in eliminatedActions)
{
decls.AddRange(GenerateStepChecker(elim));
}
Expand Down
2 changes: 1 addition & 1 deletion Source/Concurrency/MoverCheck.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -83,7 +83,7 @@ where first.IsRightMover || second.IsLeftMover

foreach (var sequentialization in civlTypeChecker.Sequentializations)
{
foreach (var leftMover in sequentialization.Abstractions)
foreach (var leftMover in sequentialization.EliminatedActions)
{
foreach (var action in civlTypeChecker.MoverActions.Where(x => x.LayerRange.Contains(sequentialization.Layer)))
{
Expand Down
73 changes: 4 additions & 69 deletions Source/Core/AST/Absy.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2909,36 +2909,12 @@ public enum MoverType
None
}

public class ElimDecl : Absy
{
public ActionDeclRef Target;
public ActionDeclRef Abstraction;

public ElimDecl(IToken tok, ActionDeclRef target, ActionDeclRef abstraction) : base(tok)
{
this.Target = target;
this.Abstraction = abstraction;
}

public override void Resolve(ResolutionContext rc)
{
Target.Resolve(rc);
Abstraction.Resolve(rc);
}

public override void Typecheck(TypecheckingContext tc)
{
throw new NotImplementedException();
}
}

public class ActionDecl : Procedure
{
public MoverType MoverType;
public List<ActionDeclRef> Creates;
public ActionDeclRef RefinedAction;
public ActionDeclRef InvariantAction;
public List<ElimDecl> Eliminates;
public List<CallCmd> YieldRequires;
public DatatypeTypeCtorDecl PendingAsyncCtorDecl;

Expand All @@ -2948,7 +2924,7 @@ public class ActionDecl : Procedure
public ActionDecl(IToken tok, string name, MoverType moverType,
List<Variable> inParams, List<Variable> outParams, bool isPure,
List<ActionDeclRef> creates, ActionDeclRef refinedAction, ActionDeclRef invariantAction,
List<ElimDecl> eliminates, List<Requires> requires, List<CallCmd> yieldRequires,
List<Requires> requires, List<CallCmd> yieldRequires,
List<IdentifierExpr> modifies, DatatypeTypeCtorDecl pendingAsyncCtorDecl, QKeyValue kv) : base(tok, name,
new List<TypeVariable>(), inParams, outParams,
isPure, requires, modifies, new List<Ensures>(), kv)
Expand All @@ -2957,7 +2933,6 @@ public ActionDecl(IToken tok, string name, MoverType moverType,
this.Creates = creates;
this.RefinedAction = refinedAction;
this.InvariantAction = invariantAction;
this.Eliminates = eliminates;
this.YieldRequires = yieldRequires;
this.PendingAsyncCtorDecl = pendingAsyncCtorDecl;
}
Expand Down Expand Up @@ -3018,21 +2993,6 @@ public override void Resolve(ResolutionContext rc)
{
InvariantAction.Resolve(rc);
}
Eliminates.ForEach(elim =>
{
elim.Resolve(rc);
});
if (Eliminates.Any())
{
if (RefinedAction == null)
{
rc.Error(this, "eliminates clause must be accompanied by refinement specification");
}
if (Eliminates.Select(elim => elim.Target.ActionDecl).Distinct().Count() != Eliminates.Count)
{
rc.Error(this, "each eliminates pair must be distinct in the first action");
}
}
}

public override void Typecheck(TypecheckingContext tc)
Expand Down Expand Up @@ -3109,26 +3069,6 @@ public override void Typecheck(TypecheckingContext tc)
tc.Error(this, $"modifies of {elimProc.Name} must be subset of modifies of {invariantActionDecl.Name}");
}
}
foreach (var elimDecl in Eliminates)
{
var targetActionDecl = elimDecl.Target.ActionDecl;
var abstractionActionDecl = elimDecl.Abstraction.ActionDecl;
var targetModifies = new HashSet<Variable>(targetActionDecl.Modifies.Select(ie => ie.Decl));
var absModifies = new HashSet<Variable>(abstractionActionDecl.Modifies.Select(ie => ie.Decl));
if (!invariantCreates.Contains(targetActionDecl))
{
tc.Error(this, $"eliminated action must be created by invariant {InvariantAction.ActionName}");
}
if (!abstractionActionDecl.LayerRange.Contains(layer))
{
tc.Error(elimDecl, $"action {abstractionActionDecl.Name} does not exist at layer {layer}");
}
if (!absModifies.IsSubsetOf(targetModifies))
{
tc.Error(elimDecl,
$"modifies of {abstractionActionDecl.Name} must be subset of modifies of {targetActionDecl.Name}");
}
}
}
}
}
Expand Down Expand Up @@ -3185,7 +3125,7 @@ protected override void EmitEnd(TokenTextWriter stream, int level)
base.EmitEnd(stream, level);
}

public Dictionary<ActionDecl, ActionDecl> EliminationMap()
public IEnumerable<ActionDecl> EliminatedActionDecls()
{
var refinedProc = RefinedAction.ActionDecl;
var refinedActionCreates = refinedProc.CreateActionDecls.ToHashSet();
Expand All @@ -3202,13 +3142,8 @@ HashSet<ActionDecl> FixpointCreates()
}
var allCreates = InvariantAction == null
? FixpointCreates()
: InvariantAction.ActionDecl.CreateActionDecls.ToHashSet();
var elimMap = allCreates.Except(refinedActionCreates).ToDictionary(x => x, x => x);
foreach (var elimDecl in Eliminates)
{
elimMap[elimDecl.Target.ActionDecl] = elimDecl.Abstraction.ActionDecl;
}
return elimMap;
: InvariantAction.ActionDecl.CreateActionDecls;
return allCreates.Except(refinedActionCreates);
}

public IEnumerable<ActionDeclRef> ActionDeclRefs()
Expand Down
Loading

0 comments on commit 4b8a095

Please sign in to comment.