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] Removed ElimDecl #873

Merged
merged 1 commit into from
Apr 22, 2024
Merged

[Civl] Removed ElimDecl #873

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
7 changes: 1 addition & 6 deletions Source/Concurrency/CivlTypeChecker.cs
View file
Open in desktop
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
Open in desktop
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
Open in desktop
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
Open in desktop
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
Loading