-
-
Notifications
You must be signed in to change notification settings - Fork 194
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Re-defined constants are not "in-lined" but re-evaluated on *every*
invocation (needs more aggressive constant propagation). Addresses Github issue #648 #648 [Feature][TLC]
- Loading branch information
Showing
10 changed files
with
340 additions
and
19 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
131 changes: 131 additions & 0 deletions
131
tlatools/org.lamport.tlatools/src/tlc2/module/TLCEval.java
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,131 @@ | ||
| /******************************************************************************* | ||
| * Copyright (c) 2022 Microsoft Research. All rights reserved. | ||
| * | ||
| * The MIT License (MIT) | ||
| * | ||
| * Permission is hereby granted, free of charge, to any person obtaining a copy | ||
| * of this software and associated documentation files (the "Software"), to deal | ||
| * in the Software without restriction, including without limitation the rights | ||
| * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies | ||
| * of the Software, and to permit persons to whom the Software is furnished to do | ||
| * so, subject to the following conditions: | ||
| * | ||
| * The above copyright notice and this permission notice shall be included in all | ||
| * copies or substantial portions of the Software. | ||
| * | ||
| * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR | ||
| * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS | ||
| * FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR | ||
| * COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN | ||
| * AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION | ||
| * WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. | ||
| * | ||
| * Contributors: | ||
| * Markus Alexander Kuppe - initial API and implementation | ||
| ******************************************************************************/ | ||
| package tlc2.module; | ||
|
|
||
| import java.util.concurrent.locks.ReadWriteLock; | ||
| import java.util.concurrent.locks.ReentrantReadWriteLock; | ||
|
|
||
| import tla2sany.semantic.ExprOrOpArgNode; | ||
| import tla2sany.semantic.LevelConstants; | ||
| import tlc2.overrides.Evaluation; | ||
| import tlc2.tool.TLCState; | ||
| import tlc2.tool.coverage.CostModel; | ||
| import tlc2.tool.impl.Tool; | ||
| import tlc2.tool.impl.WorkerValue; | ||
| import tlc2.util.Context; | ||
| import tlc2.value.ValueConstants; | ||
| import tlc2.value.impl.Value; | ||
|
|
||
| public class TLCEval implements ValueConstants { | ||
|
|
||
| public static final long serialVersionUID = 20220105L; | ||
|
|
||
| private static final ReadWriteLock lock = new ReentrantReadWriteLock(); | ||
|
|
||
| private static Value convert(final Value eval) { | ||
| // Legacy implementation of TLCEval taken from TLC.java | ||
| Value evalVal = eval.toSetEnum(); | ||
| if (evalVal != null) { | ||
| return evalVal; | ||
| } | ||
| evalVal = eval.toFcnRcd(); | ||
| if (evalVal != null) { | ||
| return evalVal; | ||
| } | ||
| return eval; | ||
| } | ||
|
|
||
| /** | ||
| * Implements TLCEval, which causes TLC to eagerly evaluate the value. Useful | ||
| * for preventing inefficiency caused by lazy evaluation defeating efforts at | ||
| * common subexpression elimination. | ||
| */ | ||
| @Evaluation(definition = "TLCEval", module = "TLC", warn = false, silent = true) | ||
| public static Value tlcEval(final Tool tool, final ExprOrOpArgNode[] args, final Context c, final TLCState s0, | ||
| final TLCState s1, final int control, final CostModel cm) { | ||
| // TLCEval has a single parameter: | ||
| final ExprOrOpArgNode arg = args[0]; | ||
|
|
||
| if (arg.getLevel() > LevelConstants.ConstantLevel) { | ||
| // For a non-constant expression, all we can do is to evaluate | ||
| // and convert the value according to the old implementation | ||
| // of TLCEval. | ||
| // Since there is no sharing going on, there is no need to deal | ||
| // with WorkerValue here. | ||
|
|
||
| // The value that a constant-level expression evaluates to is stored in the | ||
| // semantic graph. | ||
| // For a state-level formula, the value could be kept in a transient member | ||
| // of the state. This effort doesn't seem worth it, though. | ||
| return convert(tool.eval(arg, c, s0, s1, control, cm)); | ||
| } else if (!c.isEmpty()) { | ||
| // If a constant expression has a context, e.g. a parameter, we | ||
| // cannot cache the value. | ||
| return convert(tool.eval(arg, c, s0, s1, control, cm)); | ||
| } | ||
|
|
||
| return tlcEvalConst(tool, arg, cm); | ||
| } | ||
|
|
||
| private static Value tlcEvalConst(Tool tool, ExprOrOpArgNode arg, CostModel cm) { | ||
| assert arg.getLevel() == LevelConstants.ConstantLevel; | ||
|
|
||
| lock.readLock().lock(); | ||
|
|
||
| // Read with ReadLock | ||
| Object obj = WorkerValue.mux(arg.getToolObject(tool.getId())); | ||
| if (obj != null) { | ||
| // Return the cached value. | ||
| try { | ||
| return (Value) obj; | ||
| } finally { | ||
| lock.readLock().unlock(); | ||
| } | ||
| } | ||
|
|
||
| // Slow-path below. Note that ReentrantRWLock deadlocks when | ||
| // upgrading a read to a write-lock, but we don't need this here. | ||
| lock.readLock().unlock(); | ||
|
|
||
| lock.writeLock().lock(); | ||
| try { | ||
| // Re-read with WriteLock in case another thread obtained | ||
| // the write lock while this thread waited. | ||
| obj = WorkerValue.mux(arg.getToolObject(tool.getId())); | ||
| if (obj != null) { | ||
| return (Value) obj; | ||
| } | ||
|
|
||
| // Create/Write the value! | ||
| Value eval = (Value) WorkerValue.demux(tool, arg, cm); | ||
| eval = convert(eval); | ||
| arg.setToolObject(tool.getId(), eval); | ||
| return eval; | ||
| } finally { | ||
| lock.writeLock().unlock(); | ||
| } | ||
| } | ||
| } |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,4 @@ | ||
| INIT Init | ||
| NEXT Next | ||
| INVARIANT Inv | ||
| CONSTANT Graph <- TestGraph |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,51 @@ | ||
| --------------------- MODULE Github648 ----------------------------- | ||
| EXTENDS TLC, Naturals, Sequences, FiniteSets | ||
|
|
||
| BoundedSeqTLCEval(S, n) == | ||
| \* The TLCEval here must not cache the value, because it depends on the | ||
| \* context, ie. S and n. | ||
| UNION {TLCEval([1..m -> S]) : m \in 0..n} | ||
|
|
||
| ASSUME Cardinality(BoundedSeqTLCEval(BoundedSeqTLCEval({1,2}, 2), 2)) = 57 | ||
|
|
||
| ----------------------------------------------------------------------------- | ||
| BoundedSeq(S, n) == | ||
| UNION {[1..m -> S] : m \in 0..n} | ||
|
|
||
| ----------------------------------------------------------------------------- | ||
| DirectedGraphs(nodes) == | ||
| [edge : SUBSET (nodes \X nodes)] | ||
|
|
||
| TestGraph == | ||
| \* The definition of TestGraph is evaluated multiple times. If the def. | ||
| \* involves TLC!RandomElement or Randomization!* the invariant Inv below | ||
| \* will be violated *without* the TLCEval. | ||
| TLCEval( | ||
| LET g == RandomElement(DirectedGraphs(1..3)) | ||
| IN [ edge |-> g.edge \cup {<<1,1>>} ] | ||
| ) | ||
|
|
||
| ----------------------------------------------------------------------------- | ||
| CONSTANT Graph | ||
|
|
||
| VARIABLE v, w | ||
| vars == <<v, w>> | ||
|
|
||
| Init == | ||
| /\ v \in Graph.edge | ||
| /\ w \in Graph.edge | ||
|
|
||
| Next == | ||
| /\ v' \in Graph.edge | ||
| /\ w' \in Graph.edge | ||
|
|
||
| Inv == | ||
| /\ v \in Graph.edge | ||
| /\ v \in TestGraph.edge | ||
| /\ w \in Graph.edge | ||
| /\ w \in TestGraph.edge | ||
| /\ TLCEval(Cardinality( | ||
| TLCEval(BoundedSeq( | ||
| TLCEval(BoundedSeq({1,2,3}, 3)), 3)))) = 65641 | ||
|
|
||
| ============================================================================= |
Oops, something went wrong.
7d936f2There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
@Calvin-L Can you please review 7d936f2#diff-1a5eb4bed92d033811451bbc6a346f43b221d96e70a546b948f40c444257b549R67-R130 ?
7d936f2There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This looks fine to me.
RandomElementseems like a very tricky feature to support in a language where expressions are mathematical formulas and not programs... what's here seems like a reasonable enough approach, given that TLC already supportsRandomElement.7d936f2There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Archiving the specs here that were used as part of this work: