Skip to content

[Civl] Remove pending asyncs and inductive sequentialization #1091

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

Merged
shazqadeer merged 4 commits into from
Jan 20, 2026
+604 −2,509
Merged

[Civl] Remove pending asyncs and inductive sequentialization #1091

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
1325735
removed examples
shazqadeer Jan 19, 2026
31602ab
removed pending asyncs
shazqadeer Jan 19, 2026
88db81a
workaround for some batch_mode nonsense
shazqadeer Jan 19, 2026
f283180
renamed local variable to be distinct from global variable
shazqadeer Jan 20, 2026
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
70 changes: 70 additions & 0 deletions Source/Concurrency/ActionRefinement.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,70 @@
using System.Collections.Generic;
using System.Linq;

namespace Microsoft.Boogie
{
public class ActionRefinement
{
private CivlTypeChecker civlTypeChecker;
private Action targetAction;
private Implementation inlinedImpl;

public static void AddCheckers(CivlTypeChecker civlTypeChecker, List<Declaration> decls)
{
foreach (var x in civlTypeChecker.ActionRefinements)
{
decls.AddRange([x.inlinedImpl, x.inlinedImpl.Proc]);
}
}

public ActionRefinement(CivlTypeChecker civlTypeChecker, Action targetAction)
{
this.civlTypeChecker = civlTypeChecker;
this.targetAction = targetAction;
inlinedImpl = CreateInlinedImplementation();
var refinedAction = targetAction.RefinedAction;
Dictionary<Variable, Expr> map = new Dictionary<Variable, Expr>();
for (int i = 0; i < refinedAction.Impl.InParams.Count; i++)
{
map[refinedAction.Impl.InParams[i]] = Expr.Ident(inlinedImpl.Proc.InParams[i]);
}
for (int i = 0; i < refinedAction.Impl.OutParams.Count; i++)
{
map[refinedAction.Impl.OutParams[i]] = Expr.Ident(inlinedImpl.Proc.OutParams[i]);
}
var subst = Substituter.SubstitutionFromDictionary(map);
inlinedImpl.Proc.Requires = refinedAction.Gate.Select(g => new Requires(false, Substituter.Apply(subst, g.Expr))).ToList();
var frame = new HashSet<Variable>(civlTypeChecker.GlobalVariablesAtLayer(targetAction.LayerRange.UpperLayer));
inlinedImpl.Proc.Ensures = new List<Ensures>(new[]
{
new Ensures(false, Substituter.Apply(subst, refinedAction.GetTransitionRelation(civlTypeChecker, frame)))
{ Description = new FailureOnlyDescription($"Refinement check of {targetAction.Name} failed") }
});
}

private Implementation CreateInlinedImplementation()
{
var decls = new List<Declaration>();
var inlinedImpl = Action.CreateDuplicateImplementation(targetAction.ActionDecl.Impl,
$"{targetAction.ActionDecl.Name}_RefinementCheck");
CivlAttributes.RemoveAttributes(inlinedImpl.Proc, new HashSet<string> { "inline" });
decls.Add(inlinedImpl);
decls.Add(inlinedImpl.Proc);
var oldTopLevelDeclarations = new List<Declaration>(civlTypeChecker.program.TopLevelDeclarations);
civlTypeChecker.program.AddTopLevelDeclarations(decls);
decls.OfType<Implementation>().ForEach(impl =>
{
impl.OriginalBlocks = impl.Blocks;
impl.OriginalLocVars = impl.LocVars;
});
Inliner.ProcessImplementation(civlTypeChecker.Options, civlTypeChecker.program, inlinedImpl);
civlTypeChecker.program.TopLevelDeclarations = oldTopLevelDeclarations;
decls.OfType<Implementation>().ForEach(impl =>
{
impl.OriginalBlocks = null;
impl.OriginalLocVars = null;
});
return inlinedImpl;
}
}
}
199 changes: 1 addition & 198 deletions Source/Concurrency/CivlCoreTypes.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,5 +1,4 @@
using System.Collections.Generic;
using System.Diagnostics;
using System.Linq;

namespace Microsoft.Boogie
Expand All @@ -20,36 +19,12 @@ public class Action
public List<AssertCmd> SecondGate;
public Implementation SecondImpl;
public Dictionary<Variable, Function> TriggerFunctions;

public DatatypeTypeCtorDecl ChoiceDatatypeTypeCtorDecl;
public Implementation ImplWithChoice;
public Function InputOutputRelationWithChoice;

public Action(CivlTypeChecker civlTypeChecker, ActionDecl actionDecl, Action refinedAction, bool isInvariant)
public Action(CivlTypeChecker civlTypeChecker, ActionDecl actionDecl, Action refinedAction)
{
ActionDecl = actionDecl;
RefinedAction = refinedAction;
Impl = CreateDuplicateImplementation(actionDecl.Impl, actionDecl.Name);
if (PendingAsyncs.Any())
{
DesugarCreateAsyncs(civlTypeChecker, Impl, ActionDecl);
if (isInvariant)
{
ImplWithChoice = CreateDuplicateImplementation(Impl, $"{Name}_With_Choice");
var choiceDatatypeName = $"Choice_{Name}";
ChoiceDatatypeTypeCtorDecl =
new DatatypeTypeCtorDecl(Token.NoToken, choiceDatatypeName, new List<TypeVariable>(), null);
PendingAsyncs.ForEach(elim =>
{
var field = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, elim.Name, elim.PendingAsyncType), true);
ChoiceDatatypeTypeCtorDecl.AddConstructor(Token.NoToken, $"{choiceDatatypeName}_{elim.Name}",
new List<Variable>() { field });
});
civlTypeChecker.program.AddTopLevelDeclaration(ChoiceDatatypeTypeCtorDecl);
DesugarSetChoice(civlTypeChecker, ImplWithChoice);
}
DropSetChoice(Impl);
}

AddGateSufficiencyCheckerAndHoistAsserts(civlTypeChecker);

Expand All @@ -58,10 +33,6 @@ public Action(CivlTypeChecker civlTypeChecker, ActionDecl actionDecl, Action ref
UsedGlobalVarsInAction = new HashSet<Variable>(VariableCollector.Collect(Impl).Where(x => x is GlobalVariable));

InputOutputRelation = ComputeInputOutputRelation(civlTypeChecker, Impl);
if (ImplWithChoice != null)
{
InputOutputRelationWithChoice = ComputeInputOutputRelation(civlTypeChecker, ImplWithChoice);
}

AtomicActionDuplicator.SetupCopy(this, ref FirstGate, ref FirstImpl, "first_");
AtomicActionDuplicator.SetupCopy(this, ref SecondGate, ref SecondImpl, "second_");
Expand All @@ -76,10 +47,6 @@ public Action(CivlTypeChecker civlTypeChecker, ActionDecl actionDecl, Action ref

public LayerRange LayerRange => ActionDecl.LayerRange;

public IEnumerable<ActionDecl> PendingAsyncs => ActionDecl.CreateActionDecls;

public bool HasPendingAsyncs => PendingAsyncs.Any();

public bool IsRightMover => ActionDecl.MoverType == MoverType.Right || ActionDecl.MoverType == MoverType.Both;

public bool IsLeftMover => ActionDecl.MoverType == MoverType.Left || ActionDecl.MoverType == MoverType.Both;
Expand All @@ -88,27 +55,14 @@ public Action(CivlTypeChecker civlTypeChecker, ActionDecl actionDecl, Action ref

public bool IsUnconditionalLeftMover => IsLeftMover && !ActionDecl.HasPreconditions;

public int PendingAsyncStartIndex => ActionDecl.OutParams.Count;

public bool TriviallyCommutesWith(Action other)
{
return !this.ModifiedGlobalVars.Intersect(other.UsedGlobalVarsInAction).Any() &&
!this.UsedGlobalVarsInAction.Intersect(other.ModifiedGlobalVars).Any();
}

public Variable PAs(CtorType pendingAsyncType)
{
var pendingAsyncMultisetType = TypeHelper.MapType(pendingAsyncType, Type.Int);
return Impl.OutParams.Skip(PendingAsyncStartIndex).First(v => v.TypedIdent.Type.Equals(pendingAsyncMultisetType));
}

public bool HasAssumeCmd => Impl.Blocks.Any(b => b.Cmds.Any(c => c is AssumeCmd));

public DatatypeConstructor ChoiceConstructor(CtorType pendingAsyncType)
{
return ChoiceDatatypeTypeCtorDecl.Constructors.First(x => x.InParams[0].TypedIdent.Type.Equals(pendingAsyncType));
}

public IEnumerable<AssertCmd> GetGateAsserts(Substitution subst, string msg)
{
foreach (var gate in Gate)
Expand All @@ -124,30 +78,6 @@ public Expr GetTransitionRelation(CivlTypeChecker civlTypeChecker, HashSet<Varia
return TransitionRelationComputation.Refinement(civlTypeChecker, Impl, frame);
}

public Substitution GetSubstitution(Action to)
{
Debug.Assert(PendingAsyncStartIndex == to.PendingAsyncStartIndex);
Debug.Assert(Impl.InParams.Count == to.Impl.InParams.Count);
Debug.Assert(Impl.OutParams.Count <= to.Impl.OutParams.Count);

Dictionary<Variable, Expr> map = new Dictionary<Variable, Expr>();
for (int i = 0; i < Impl.InParams.Count; i++)
{
map[Impl.InParams[i]] = Expr.Ident(to.Impl.InParams[i]);
}
for (int i = 0; i < PendingAsyncStartIndex; i++)
{
map[Impl.OutParams[i]] = Expr.Ident(to.Impl.OutParams[i]);
}
for (int i = PendingAsyncStartIndex; i < Impl.OutParams.Count; i++)
{
var formal = Impl.OutParams[i];
var pendingAsyncType = (CtorType)((MapType)formal.TypedIdent.Type).Arguments[0];
map[formal] = Expr.Ident(to.PAs(pendingAsyncType));
}
return Substituter.SubstitutionFromDictionary(map);
}

public IEnumerable<AssertCmd> Preconditions(int layerNum, Substitution subst)
{
var errorMessage = $"this precondition of {Name} could not be proved";
Expand Down Expand Up @@ -265,133 +195,6 @@ private Function ComputeInputOutputRelation(CivlTypeChecker civlTypeChecker, Imp
CivlUtil.ResolveAndTypecheck(civlTypeChecker.Options, inputOutputRelation.Body);
return inputOutputRelation;
}

public static void DesugarCreateAsyncs(CivlTypeChecker civlTypeChecker, Implementation impl, ActionDecl actionDecl)
{
Debug.Assert(impl.OutParams.Count == actionDecl.OutParams.Count);
var pendingAsyncTypeToActionDecl = new Dictionary<CtorType, ActionDecl>();
var lhss = new List<IdentifierExpr>();
var rhss = new List<Expr>();
actionDecl.CreateActionDecls.ForEach(decl =>
{
pendingAsyncTypeToActionDecl[decl.PendingAsyncType] = decl;
var pa = civlTypeChecker.Formal($"PAs_{decl.Name}", decl.PendingAsyncMultisetType, false);
impl.Proc.OutParams.Add(pa);
impl.OutParams.Add(pa);
lhss.Add(Expr.Ident(pa));
rhss.Add(ExprHelper.FunctionCall(decl.PendingAsyncConst, Expr.Literal(0)));
});
var tc = new TypecheckingContext(null, civlTypeChecker.Options);
var initAssignCmd = CmdHelper.AssignCmd(lhss, rhss);
initAssignCmd.Typecheck(tc);
impl.Blocks[0].Cmds.Insert(0, initAssignCmd);
impl.Blocks.ForEach(block =>
{
var newCmds = new List<Cmd>();
foreach (var cmd in block.Cmds)
{
if (cmd is CallCmd callCmd)
{
var originalProc = (Procedure)Monomorphizer.GetOriginalDecl(callCmd.Proc);
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_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));
updateAssignCmd.Typecheck(tc);
newCmds.Add(updateAssignCmd);
continue;
}
}
newCmds.Add(cmd);
}
block.Cmds = newCmds;
});
}

private void DropSetChoice(Implementation impl)
{
impl.Blocks.ForEach(block =>
{
var newCmds = new List<Cmd>();
foreach (var cmd in block.Cmds)
{
if (cmd is CallCmd callCmd)
{
var originalProcName = Monomorphizer.GetOriginalDecl(callCmd.Proc).Name;
if (originalProcName == "set_choice")
{
continue;
}
}
newCmds.Add(cmd);
}
block.Cmds = newCmds;
});
}

private void DesugarSetChoice(CivlTypeChecker civlTypeChecker, Implementation impl)
{
var choice = civlTypeChecker.Formal("choice", TypeHelper.CtorType(ChoiceDatatypeTypeCtorDecl), false);
impl.Proc.OutParams.Add(choice);
impl.OutParams.Add(choice);
impl.Blocks.ForEach(block =>
{
var newCmds = new List<Cmd>();
foreach (var cmd in block.Cmds)
{
if (cmd is CallCmd callCmd)
{
var originalProcName = Monomorphizer.GetOriginalDecl(callCmd.Proc).Name;
if (originalProcName == "set_choice")
{
var pendingAsyncType = (CtorType)civlTypeChecker.program.monomorphizer.GetTypeInstantiation(callCmd.Proc)["T"];
var pendingAsync = PendingAsyncs.First(decl => decl.PendingAsyncType.Equals(pendingAsyncType));
var tc = new TypecheckingContext(null, civlTypeChecker.Options);
var emptyExpr = Expr.Eq(Expr.Ident(PAs(pendingAsyncType)),
ExprHelper.FunctionCall(pendingAsync.PendingAsyncConst, Expr.Literal(0)));
var memberExpr = Expr.Gt(Expr.Select(Expr.Ident(PAs(pendingAsyncType)), callCmd.Ins[0]),
Expr.Literal(0));
var assertCmd = CmdHelper.AssertCmd(cmd.tok, Expr.Or(emptyExpr, memberExpr),
"Choice is not a created pending async");
assertCmd.Typecheck(tc);
newCmds.Add(assertCmd);
var assignCmd = CmdHelper.AssignCmd(CmdHelper.FieldAssignLhs(Expr.Ident(choice), pendingAsyncType.Decl.Name), callCmd.Ins[0]);
assignCmd.Typecheck(tc);
newCmds.Add(assignCmd);
continue;
}
}
newCmds.Add(cmd);
}
block.Cmds = newCmds;
});
}

private void DeclareTriggerFunctions()
{
Expand Down
10 changes: 1 addition & 9 deletions Source/Concurrency/CivlRewriter.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -29,11 +29,6 @@ public static void Transform(ConcurrencyOptions options, CivlTypeChecker civlTyp
civlTypeChecker.AtomicActions.ForEach(x =>
{
decls.AddRange(new Declaration[] { x.Impl, x.Impl.Proc, x.InputOutputRelation });
if (x.ImplWithChoice != null)
{
decls.AddRange(new Declaration[]
{ x.ImplWithChoice, x.ImplWithChoice.Proc, x.InputOutputRelationWithChoice });
}
});

// Commutativity checks
Expand All @@ -51,10 +46,7 @@ public static void Transform(ConcurrencyOptions options, CivlTypeChecker civlTyp
if (!options.TrustRefinement)
{
YieldingProcChecker.AddRefinementCheckers(civlTypeChecker, decls);
if (!options.TrustSequentialization)
{
Sequentialization.AddCheckers(civlTypeChecker, decls);
}
ActionRefinement.AddCheckers(civlTypeChecker, decls);
}

foreach (var action in civlTypeChecker.AtomicActions)
Expand Down
Loading
Loading