From 7350a2afe8b37c7ee02fd99b5069a03e982b74d8 Mon Sep 17 00:00:00 2001 From: Shaz Qadeer Date: Fri, 3 Apr 2020 10:05:50 -0700 Subject: [PATCH] - added async precondition checkers (#216) - some renaming and documentation - disabled linear type checking in introduction procedures --- Source/Concurrency/CivlVCGeneration.cs | 2 +- Source/Concurrency/LinearTypeChecker.cs | 20 ++++++++++--------- Source/Concurrency/YieldingProcDuplicator.cs | 11 +++++----- .../YieldingProcInstrumentation.cs | 8 ++++---- 4 files changed, 22 insertions(+), 19 deletions(-) diff --git a/Source/Concurrency/CivlVCGeneration.cs b/Source/Concurrency/CivlVCGeneration.cs index 96514430d..884ba5f2c 100644 --- a/Source/Concurrency/CivlVCGeneration.cs +++ b/Source/Concurrency/CivlVCGeneration.cs @@ -42,7 +42,7 @@ public static void Transform(CivlTypeChecker civlTypeChecker) BackwardAssignmentSubstituter.SubstituteBackwardAssignments(civlTypeChecker.procToAtomicAction.Values); - linearTypeChecker.Transform(); + linearTypeChecker.AddDeclarations(); linearTypeChecker.EraseLinearAnnotations(); } } diff --git a/Source/Concurrency/LinearTypeChecker.cs b/Source/Concurrency/LinearTypeChecker.cs index 664bb04a3..efad89c39 100644 --- a/Source/Concurrency/LinearTypeChecker.cs +++ b/Source/Concurrency/LinearTypeChecker.cs @@ -286,8 +286,10 @@ private void MapLeInt() /// The functionality is basically grouped into four parts (see #region's). /// 1) TypeCheck parses linear type attributes, sets up the data structures, /// and performs a dataflow check on procedure implementations. - /// 2) Generation of linearity-invariant checker procedures for atomic actions. - /// 3) Erasure procedure to remove all linearity attributes + /// 2) Useful public methods to generate expressions for permissions, their disjointness, + /// and their union. + /// 3) Generation of linearity-invariant checker procedures for atomic actions. + /// 4) Erasure procedure to remove all linearity attributes /// (invoked after all other CIVL transformations). /// public class LinearTypeChecker : ReadOnlyVisitor @@ -296,7 +298,7 @@ public class LinearTypeChecker : ReadOnlyVisitor public CheckingContext checkingContext; public Dictionary linearDomains; - private CivlTypeChecker ctc; + private CivlTypeChecker civlTypeChecker; private Dictionary> availableLinearVars; private Dictionary inParamToLinearQualifier; @@ -307,11 +309,11 @@ public class LinearTypeChecker : ReadOnlyVisitor private Dictionary> domainNameToCollectors; private Dictionary varToDomainName; - public LinearTypeChecker(CivlTypeChecker ctc) + public LinearTypeChecker(CivlTypeChecker civlTypeChecker) { - this.ctc = ctc; - this.program = ctc.program; - this.checkingContext = ctc.checkingContext; + this.civlTypeChecker = civlTypeChecker; + this.program = civlTypeChecker.program; + this.checkingContext = civlTypeChecker.checkingContext; this.domainNameToCollectors = new Dictionary>(); this.availableLinearVars = new Dictionary>(); this.inParamToLinearQualifier = new Dictionary(); @@ -455,7 +457,7 @@ public override Function VisitFunction(Function node) } public override Implementation VisitImplementation(Implementation node) { - if (ctc.procToAtomicAction.ContainsKey(node.Proc)) + if (civlTypeChecker.procToAtomicAction.ContainsKey(node.Proc) || civlTypeChecker.procToIntroductionProc.ContainsKey(node.Proc)) return node; node.PruneUnreachableBlocks(); @@ -852,7 +854,7 @@ public override Ensures VisitEnsures(Ensures ensures) #endregion #region Useful public methods - public void Transform() + public void AddDeclarations() { foreach (LinearDomain domain in linearDomains.Values) { diff --git a/Source/Concurrency/YieldingProcDuplicator.cs b/Source/Concurrency/YieldingProcDuplicator.cs index e50152a70..c3f641be1 100644 --- a/Source/Concurrency/YieldingProcDuplicator.cs +++ b/Source/Concurrency/YieldingProcDuplicator.cs @@ -257,16 +257,16 @@ private void DesugarAsyncCall(CallCmd newCall) if (!asyncCallPreconditionCheckers.ContainsKey(newCall.Proc.Name)) { asyncCallPreconditionCheckers[newCall.Proc.Name] = new Procedure(Token.NoToken, - $"DummyAsyncTarget_{newCall.Proc.Name}", + $"AsyncCallPreconditionChecker_{newCall.Proc.Name}", newCall.Proc.TypeParameters, newCall.Proc.InParams, newCall.Proc.OutParams, newCall.Proc.Requires, new List(), new List()); } - var dummyAsyncTargetProc = asyncCallPreconditionCheckers[newCall.Proc.Name]; - CallCmd dummyCallCmd = new CallCmd(newCall.tok, dummyAsyncTargetProc.Name, newCall.Ins, + var asyncCallPreconditionChecker = asyncCallPreconditionCheckers[newCall.Proc.Name]; + CallCmd checkerCallCmd = new CallCmd(newCall.tok, asyncCallPreconditionChecker.Name, newCall.Ins, newCall.Outs, newCall.Attributes); - dummyCallCmd.Proc = dummyAsyncTargetProc; - newCmdSeq.Add(dummyCallCmd); + checkerCallCmd.Proc = asyncCallPreconditionChecker; + newCmdSeq.Add(checkerCallCmd); } private void CollectPendingAsync(CallCmd call, CallCmd newCall, ActionProc actionProc) @@ -459,6 +459,7 @@ public List Collect() decls.AddRange(procMap.Values); var newImpls = absyMap.Keys.OfType(); decls.AddRange(newImpls); + decls.AddRange(asyncCallPreconditionCheckers.Values); decls.AddRange(YieldingProcInstrumentation.TransformImplementations( civlTypeChecker, linearTypeChecker, diff --git a/Source/Concurrency/YieldingProcInstrumentation.cs b/Source/Concurrency/YieldingProcInstrumentation.cs index 8a719e4a4..9b95b4256 100644 --- a/Source/Concurrency/YieldingProcInstrumentation.cs +++ b/Source/Concurrency/YieldingProcInstrumentation.cs @@ -574,7 +574,7 @@ private List DesugarParCallCmd(ParCallCmd parCallCmd) var newCmds = new List(); List ins = new List(); List outs = new List(); - string procName = "og"; + string procName = "ParallelCallPreconditionChecker"; foreach (CallCmd callCmd in parCallCmd.CallCmds) { procName = procName + "_" + callCmd.Proc.Name; @@ -624,9 +624,9 @@ private List DesugarParCallCmd(ParCallCmd parCallCmd) } Procedure proc = parallelCallPreconditionCheckers[procName]; - CallCmd dummyCallCmd = new CallCmd(parCallCmd.tok, proc.Name, ins, outs, parCallCmd.Attributes); - dummyCallCmd.Proc = proc; - newCmds.Add(dummyCallCmd); + CallCmd checkerCallCmd = new CallCmd(parCallCmd.tok, proc.Name, ins, outs, parCallCmd.Attributes); + checkerCallCmd.Proc = proc; + newCmds.Add(checkerCallCmd); return newCmds; }