[Proof-of-Concept] Liveness checking ccfraft#6587

Draft

lemmy wants to merge 25 commits intomicrosoft:mainfrom lemmy:mku-abslive

+221-16

Commits on Jan 6, 2025

* Add Spec and SpecAxiom
lemmy
committed
* Second state constraint that binds the divergence of any two logs
lemmy
committed
Commenting AppendOnlyProp make TLC find a violation of InSync
lemmy
committed
TLC finds a valid counterexample for another *insufficient* fairness constraint:
lemmy
committed
Converting MonotonicReduction into a TLC view allows us to again verify AppendOnlyProp. However, TLC produces a bogus counterexample for InSync:
lemmy
committed
The deliberate introduction of a bug is correctly found by TLC:
lemmy
committed
No violation with a non-machine closed fairness constraint:
lemmy
committed
Replace fairness constraint that turns FairSpec => InSync into a tautology into a sufficient constraint that is not a tautology.
lemmy
committed
Note the differences of AppendOnlyProp and ccfraft's CommittedLogAppendOnlyProp.
lemmy
committed
InSync cannot be guaranteed without a non-machine-close fairness
lemmy
committed
Syntactically refactor MonotonicReduction.
lemmy
committed
Add second liveness property Syncing that mandates that the log
lemmy
committed
As expect, AllSyncing is not a theorem of the spec:
lemmy
committed
Prove abs type-correct.
lemmy
committed
The properties InSync and AllSyncing are not expected to hold for MachineClosedFairSpec.
lemmy
committed
No need to constrain the log length under a view and a bounded divergence.
lemmy
committed
Refactor liveness properties.
lemmy
committed
Refactor name of fairness constraint.
lemmy
committed
With a single node, the View reduces the state-space to a single state.
lemmy
committed
There is no (explicit) upper bound on the length of logs; explain what makes the state space finite.
lemmy
committed
Add a simpler variant of the MonotonicReduction that just drops the common prefix but leaves the Terms untouched.
lemmy
committed
0 is a bogus default that causes both MonotonicReduction* definitions
lemmy
committed
Add a leads-to property EmptyLeadsToNonEmpty to the properties we check under the MonotonicReduction view.
lemmy
committed
Properties that cause spurious counterexamples here to illustrate the limitations of the MonotonicReduction view.
lemmy
committed
Add (temporal) formulas that are expected to result in counterexamples as sanity checks.
lemmy
committed