From f7a88b5e414264a2b05e1064764ac896445ee122 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Dinis=20Ferreira?= Date: Sat, 26 Sep 2026 01:34:56 +0200 Subject: [PATCH 1/3] test(formal): add TLA+ and Lean models of five DDK subsystems Blind models of the parallel resource loader, find-references batching, the binary-model storage executor, the qualified-name trie and the release pipeline, each in TLA+ and Lean 4, with fixed variants, ablations, planted bugs and witnesses. formal/check.sh re-runs every TLC matrix against its expected.txt, builds each Lean project, rejects sorry/admit and checks the axioms of every listed theorem. Co-Authored-By: Claude Opus 5.5 --- formal/.gitignore | 27 + formal/binary-storage/lean/BinaryStorage.lean | 4 + .../lean/BinaryStorage/Check.lean | 103 +++ .../lean/BinaryStorage/Model.lean | 338 +++++++++ .../lean/BinaryStorage/Proof.lean | 120 ++++ .../lean/BinaryStorage/Results.lean | 52 ++ formal/binary-storage/lean/NOTES.md | 252 +++++++ formal/binary-storage/lean/lake-manifest.json | 6 + formal/binary-storage/lean/lakefile.toml | 6 + formal/binary-storage/lean/lean-toolchain | 1 + formal/binary-storage/lean/theorems.txt | 20 + formal/binary-storage/tla/BinaryStorage.tla | 488 +++++++++++++ formal/binary-storage/tla/MC.tla | 16 + formal/binary-storage/tla/NOTES.md | 189 +++++ formal/binary-storage/tla/cfg/ablateA.cfg | 25 + formal/binary-storage/tla/cfg/ablateB.cfg | 25 + formal/binary-storage/tla/cfg/ablateC.cfg | 25 + formal/binary-storage/tla/cfg/ablateD.cfg | 25 + formal/binary-storage/tla/cfg/fixed_L.cfg | 28 + formal/binary-storage/tla/cfg/fixed_L2.cfg | 25 + formal/binary-storage/tla/cfg/fixed_M.cfg | 28 + formal/binary-storage/tla/cfg/fixed_M2.cfg | 28 + formal/binary-storage/tla/cfg/fixed_R.cfg | 28 + formal/binary-storage/tla/cfg/fixed_S.cfg | 28 + .../tla/cfg/happy_LoaderNoPartialRead.cfg | 18 + .../tla/cfg/happy_MainNoPartialRead.cfg | 18 + .../tla/cfg/happy_NoDetachedStore.cfg | 18 + .../tla/cfg/happy_NoStaleRead.cfg | 18 + .../tla/cfg/happy_NotSourceOnlyWhenStored.cfg | 18 + .../tla/cfg/happy_SetThreadSafe.cfg | 18 + .../tla/cfg/orig_LoaderNoPartialRead.cfg | 18 + .../tla/cfg/orig_MainNoPartialRead.cfg | 18 + .../tla/cfg/orig_NoDetachedStore.cfg | 18 + .../tla/cfg/orig_NoStaleRead.cfg | 18 + .../tla/cfg/orig_NotSourceOnlyWhenStored.cfg | 18 + .../binary-storage/tla/cfg/orig_P1_nofail.cfg | 18 + .../tla/cfg/orig_SetThreadSafe.cfg | 18 + .../tla/cfg/orig_StoresAccounted.cfg | 18 + formal/binary-storage/tla/cfg/orig_TypeOK.cfg | 18 + formal/binary-storage/tla/cfg/orig_adr.cfg | 18 + .../tla/cfg/orig_detached_nolinkfail.cfg | 18 + formal/binary-storage/tla/cfg/orig_live.cfg | 20 + formal/binary-storage/tla/cfg/orig_live_M.cfg | 20 + .../tla/cfg/orig_loaderpartial_M.cfg | 18 + .../tla/cfg/orig_mainpartial.cfg | 18 + formal/binary-storage/tla/cfg/orig_rdw.cfg | 18 + .../tla/cfg/orig_stale_nofail.cfg | 18 + formal/binary-storage/tla/cfg/planted.cfg | 25 + formal/binary-storage/tla/cfg/smoke.cfg | 18 + .../tla/cfg/wit_fixed_WitnessCallerRuns.cfg | 18 + .../tla/cfg/wit_fixed_WitnessDone.cfg | 18 + .../tla/cfg/wit_fixed_WitnessGoodRead.cfg | 18 + .../tla/cfg/wit_fixed_WitnessSecondClust.cfg | 18 + .../tla/cfg/wit_fixed_WitnessStoreOk.cfg | 18 + .../tla/cfg/wit_fixed_WitnessTimeout.cfg | 18 + .../tla/cfg/wit_orig_WitnessCallerRuns.cfg | 18 + .../tla/cfg/wit_orig_WitnessDone.cfg | 18 + .../tla/cfg/wit_orig_WitnessGoodRead.cfg | 18 + .../tla/cfg/wit_orig_WitnessSecondClust.cfg | 18 + .../tla/cfg/wit_orig_WitnessStoreOk.cfg | 18 + .../tla/cfg/wit_orig_WitnessTimeout.cfg | 18 + formal/binary-storage/tla/check_all.sh | 41 ++ formal/binary-storage/tla/expected.txt | 39 ++ formal/binary-storage/tla/gen.sh | 25 + formal/binary-storage/tla/run.sh | 6 + formal/binary-storage/tla/trace.py | 29 + formal/check.sh | 182 +++++ formal/find-refs/lean/.gitignore | 1 + formal/find-refs/lean/FindRefs.lean | 6 + formal/find-refs/lean/FindRefs/Buggy.lean | 127 ++++ formal/find-refs/lean/FindRefs/Check.lean | 106 +++ formal/find-refs/lean/FindRefs/Fixed.lean | 82 +++ formal/find-refs/lean/FindRefs/Proof.lean | 203 ++++++ formal/find-refs/lean/FindRefs/State.lean | 152 ++++ formal/find-refs/lean/FindRefs/Theorems.lean | 36 + formal/find-refs/lean/NOTES.md | 188 +++++ formal/find-refs/lean/Report.lean | 11 + formal/find-refs/lean/lake-manifest.json | 6 + formal/find-refs/lean/lakefile.toml | 5 + formal/find-refs/lean/lean-toolchain | 1 + formal/find-refs/lean/report.txt | 221 ++++++ formal/find-refs/lean/theorems.txt | 16 + formal/find-refs/tla/FindRefs.cfg | 15 + formal/find-refs/tla/FindRefs.tla | 483 +++++++++++++ formal/find-refs/tla/FindRefsFixed.cfg | 14 + formal/find-refs/tla/NOTES.md | 193 +++++ formal/find-refs/tla/coverage.sh | 14 + formal/find-refs/tla/expected.txt | 27 + formal/find-refs/tla/matrix.sh | 24 + formal/find-refs/tla/run.sh | 33 + formal/find-refs/tla/trace.py | 18 + .../fixed_minus_plock_OneRootCreated.txt | 22 + .../fixed_minus_plock_with_atomic_NoStale.txt | 48 ++ formal/find-refs/tla/traces/orig_NoCME.txt | 19 + .../find-refs/tla/traces/orig_NoDeadlock.txt | 6 + formal/find-refs/tla/traces/orig_NoDupRef.txt | 46 ++ .../find-refs/tla/traces/orig_NoForeign.txt | 23 + .../find-refs/tla/traces/orig_NoLostRef.txt | 31 + .../find-refs/tla/traces/orig_NoLostRoot.txt | 31 + .../tla/traces/orig_OneRootCreated.txt | 22 + ..._flagfixed_lost_ref_via_duplicate_root.txt | 42 ++ formal/find-refs/tla/traces/planted.txt | 22 + formal/parallel-loader/lean/.gitignore | 2 + formal/parallel-loader/lean/NOTES.md | 131 ++++ .../parallel-loader/lean/ParallelLoader.lean | 4 + .../lean/ParallelLoader/Check.lean | 116 +++ .../lean/ParallelLoader/Model.lean | 212 ++++++ .../lean/ParallelLoader/Proof.lean | 250 +++++++ .../lean/ParallelLoader/Results.lean | 104 +++ .../parallel-loader/lean/lake-manifest.json | 6 + formal/parallel-loader/lean/lakefile.toml | 6 + formal/parallel-loader/lean/lean-toolchain | 1 + formal/parallel-loader/lean/theorems.txt | 26 + formal/parallel-loader/tla/NOTES.md | 157 +++++ formal/parallel-loader/tla/ParallelLoader.cfg | 15 + formal/parallel-loader/tla/ParallelLoader.tla | 306 ++++++++ .../tla/ParallelLoaderFixed.tla | 314 +++++++++ formal/parallel-loader/tla/cfg/abort_arr1.cfg | 12 + formal/parallel-loader/tla/cfg/abort_sync.cfg | 12 + formal/parallel-loader/tla/cfg/abort_unb.cfg | 12 + .../tla/cfg/big_AbortOnlyOnCancel.cfg | 12 + .../tla/cfg/big_Bookkeeping.cfg | 12 + formal/parallel-loader/tla/cfg/bk_arr1.cfg | 12 + formal/parallel-loader/tla/cfg/bk_sync.cfg | 12 + formal/parallel-loader/tla/cfg/bk_unb.cfg | 12 + .../parallel-loader/tla/cfg/full_l_arr2.cfg | 13 + .../parallel-loader/tla/cfg/full_l_sync.cfg | 13 + formal/parallel-loader/tla/cfg/full_l_unb.cfg | 13 + .../parallel-loader/tla/cfg/full_m_arr1.cfg | 13 + .../parallel-loader/tla/cfg/full_m_sync.cfg | 13 + formal/parallel-loader/tla/cfg/full_m_unb.cfg | 13 + .../parallel-loader/tla/cfg/full_s_arr1.cfg | 13 + .../parallel-loader/tla/cfg/full_s_sync.cfg | 13 + formal/parallel-loader/tla/cfg/full_s_unb.cfg | 13 + .../parallel-loader/tla/cfg/full_xl_arr2.cfg | 13 + formal/parallel-loader/tla/cfg/leak_arr1.cfg | 12 + .../tla/cfg/live_done_arr1.cfg | 12 + .../tla/cfg/live_done_sync.cfg | 12 + .../parallel-loader/tla/cfg/live_done_unb.cfg | 12 + .../parallel-loader/tla/cfg/live_int_arr1.cfg | 12 + .../parallel-loader/tla/cfg/live_int_sync.cfg | 12 + .../parallel-loader/tla/cfg/live_int_unb.cfg | 12 + .../tla/cfg/live_noint_arr1.cfg | 12 + .../tla/cfg/live_noint_sync.cfg | 12 + .../tla/cfg/live_noint_unb.cfg | 12 + .../tla/cfg/live_swallow_arr1.cfg | 12 + .../tla/cfg/live_swallow_sync.cfg | 12 + .../tla/cfg/live_swallow_unb.cfg | 12 + .../parallel-loader/tla/cfg/planted_abort.cfg | 12 + formal/parallel-loader/tla/cfg/qc_arr1.cfg | 12 + formal/parallel-loader/tla/cfg/qc_sync.cfg | 12 + formal/parallel-loader/tla/cfg/qc_unb.cfg | 12 + formal/parallel-loader/tla/cfg/wit_m_sync.cfg | 11 + formal/parallel-loader/tla/check_all.sh | 13 + formal/parallel-loader/tla/expected.txt | 50 ++ formal/parallel-loader/tla/gen.sh | 18 + formal/parallel-loader/tla/run.sh | 6 + formal/parallel-loader/tla/trace.sh | 8 + .../tla/variants/AblateFix1.tla | 315 +++++++++ .../tla/variants/AblateFix2.tla | 314 +++++++++ .../tla/variants/AblateFix3.tla | 314 +++++++++ .../tla/variants/ParallelLoaderPlanted.tla | 314 +++++++++ formal/pipeline/lean/.gitignore | 1 + formal/pipeline/lean/NOTES.md | 180 +++++ formal/pipeline/lean/Pipeline.lean | 3 + formal/pipeline/lean/Pipeline/Check.lean | 196 ++++++ formal/pipeline/lean/Pipeline/Configs.lean | 19 + formal/pipeline/lean/Pipeline/Model.lean | 483 +++++++++++++ formal/pipeline/lean/Report.lean | 29 + formal/pipeline/lean/Results.lean | 62 ++ formal/pipeline/lean/lake-manifest.json | 6 + formal/pipeline/lean/lakefile.toml | 13 + formal/pipeline/lean/lean-toolchain | 1 + formal/pipeline/lean/report.txt | 366 ++++++++++ formal/pipeline/lean/theorems.txt | 11 + formal/pipeline/tla/NOTES.md | 318 +++++++++ formal/pipeline/tla/Pipeline.tla | 517 ++++++++++++++ .../pipeline/tla/cfg/asis_IndexNoDangling.cfg | 14 + formal/pipeline/tla/cfg/asis_LatestExists.cfg | 14 + .../tla/cfg/asis_LatestFromMaster.cfg | 14 + .../pipeline/tla/cfg/asis_MaintOnOwnLine.cfg | 14 + .../tla/cfg/asis_NoCrossRefCancel.cfg | 14 + .../pipeline/tla/cfg/asis_NoLostContent.cfg | 14 + .../pipeline/tla/cfg/asis_OwnLineVersion.cfg | 14 + .../pipeline/tla/cfg/asis_RelLatestIsMax.cfg | 14 + .../pipeline/tla/cfg/asis_RerunProgress.cfg | 14 + formal/pipeline/tla/cfg/asis_TagHasRepo.cfg | 14 + .../tla/cfg/asis_TagHasRepoOrLive.cfg | 14 + formal/pipeline/tla/cfg/asis_W_Evicted.cfg | 14 + .../pipeline/tla/cfg/asis_W_MaintRelease.cfg | 14 + .../pipeline/tla/cfg/asis_W_MasterRelease.cfg | 14 + formal/pipeline/tla/cfg/asis_live_maint.cfg | 14 + formal/pipeline/tla/cfg/asis_live_master.cfg | 14 + formal/pipeline/tla/cfg/asis_live_tags.cfg | 14 + .../pipeline/tla/cfg/fix_MaintOnOwnLine.cfg | 14 + .../pipeline/tla/cfg/fix_W_CalmGoal_maint.cfg | 14 + formal/pipeline/tla/cfg/fix_W_Evicted.cfg | 14 + .../pipeline/tla/cfg/fix_W_MaintRelease.cfg | 14 + .../pipeline/tla/cfg/fix_W_MasterRelease.cfg | 14 + formal/pipeline/tla/cfg/fix_live_maint.cfg | 15 + formal/pipeline/tla/cfg/fix_live_master.cfg | 15 + .../pipeline/tla/cfg/fix_relLatest_ctrl.cfg | 14 + formal/pipeline/tla/cfg/fix_safety.cfg | 22 + formal/pipeline/tla/cfg/fix_safety_d3.cfg | 21 + formal/pipeline/tla/cfg/fix_safety_maint.cfg | 22 + formal/pipeline/tla/cfg/fix_safety_wide.cfg | 22 + formal/pipeline/tla/cfg/plant_cleanup.cfg | 14 + formal/pipeline/tla/cfg/plant_relLatest.cfg | 14 + formal/pipeline/tla/expected.txt | 30 + formal/pipeline/tla/run.sh | 34 + formal/pipeline/tla/run_all.sh | 34 + formal/pipeline/tla/trace.py | 48 ++ formal/readonly/comparator/MinSize.java | 20 + formal/readonly/comparator/Runner.java | 42 ++ .../orphans/check-test-reachability.sh | 212 ++++++ formal/readonly/orphans/expected.txt | 5 + formal/readonly/orphans/selftest.sh | 133 ++++ formal/trie/lean/.gitignore | 3 + formal/trie/lean/Main.lean | 56 ++ formal/trie/lean/NOTES.md | 243 +++++++ formal/trie/lean/Trie.lean | 10 + formal/trie/lean/Trie/Axioms.lean | 19 + formal/trie/lean/Trie/Basic.lean | 89 +++ formal/trie/lean/Trie/Checks.lean | 347 +++++++++ formal/trie/lean/Trie/Consumer.lean | 51 ++ formal/trie/lean/Trie/Domains.lean | 47 ++ formal/trie/lean/Trie/Fixed.lean | 122 ++++ formal/trie/lean/Trie/Pattern.lean | 186 +++++ formal/trie/lean/Trie/Theorems.lean | 228 ++++++ formal/trie/lean/Trie/Tree.lean | 324 +++++++++ formal/trie/lean/Trie/TreeSet.lean | 78 +++ formal/trie/lean/Trie/Validate.lean | 122 ++++ formal/trie/lean/java-check/RunTests.java | 18 + formal/trie/lean/java-check/TrieRepro.java | 97 +++ .../xtext/naming/QualifiedNamePattern.java | 464 ++++++++++++ .../QualifiedNameSegmentTreeLookup.java | 660 ++++++++++++++++++ .../PatternAwareEObjectDescriptionLookUp.java | 119 ++++ formal/trie/lean/lake-manifest.json | 6 + formal/trie/lean/lakefile.toml | 9 + formal/trie/lean/lean-toolchain | 1 + formal/trie/lean/results/axioms.txt | 26 + .../lean/results/formal-test-as-written.txt | 14 + formal/trie/lean/results/full-run.txt | 341 +++++++++ formal/trie/lean/results/java-repro.txt | 38 + .../results/junit-as-written-vs-fixed.txt | 96 +++ formal/trie/lean/theorems.txt | 56 ++ formal/trie/tla/Consumer.tla | 50 ++ formal/trie/tla/MC_Cons.tla | 14 + formal/trie/tla/MC_Ops.tla | 10 + formal/trie/tla/MC_TQ.tla | 20 + formal/trie/tla/MC_TQ2.tla | 17 + formal/trie/tla/NOTES.md | 163 +++++ formal/trie/tla/PatternBounds.tla | 50 ++ formal/trie/tla/QNBase.tla | 211 ++++++ formal/trie/tla/TrieCore.tla | 109 +++ formal/trie/tla/TrieOps.tla | 165 +++++ formal/trie/tla/TrieQuery.tla | 55 ++ formal/trie/tla/cfg/co_ci.cfg | 5 + formal/trie/tla/cfg/co_ci_fb.cfg | 5 + formal/trie/tla/cfg/co_cs.cfg | 5 + formal/trie/tla/cfg/co_cs_fb.cfg | 5 + formal/trie/tla/cfg/co_fixed.cfg | 5 + formal/trie/tla/cfg/co_wit.cfg | 5 + formal/trie/tla/cfg/op_bagns.cfg | 6 + formal/trie/tla/cfg/op_copy.cfg | 6 + formal/trie/tla/cfg/op_exact.cfg | 6 + formal/trie/tla/cfg/op_exactref.cfg | 6 + formal/trie/tla/cfg/op_fixed.cfg | 6 + formal/trie/tla/cfg/op_fixed5.cfg | 6 + formal/trie/tla/cfg/op_fixed_sh.cfg | 6 + formal/trie/tla/cfg/op_fixed_sh5.cfg | 6 + formal/trie/tla/cfg/op_map.cfg | 6 + formal/trie/tla/cfg/op_nodup.cfg | 6 + formal/trie/tla/cfg/op_plant.cfg | 6 + formal/trie/tla/cfg/op_share.cfg | 6 + formal/trie/tla/cfg/op_sizespec.cfg | 6 + formal/trie/tla/cfg/op_sizetree.cfg | 6 + formal/trie/tla/cfg/op_wit1.cfg | 6 + formal/trie/tla/cfg/op_wit2.cfg | 6 + formal/trie/tla/cfg/pb_cnt.cfg | 5 + formal/trie/tla/cfg/pb_cnt1.cfg | 5 + formal/trie/tla/cfg/pb_fixed.cfg | 5 + formal/trie/tla/cfg/pb_ord.cfg | 5 + formal/trie/tla/cfg/pb_plant.cfg | 5 + formal/trie/tla/cfg/pb_rs.cfg | 5 + formal/trie/tla/cfg/pb_rs2.cfg | 5 + formal/trie/tla/cfg/pb_ts.cfg | 5 + formal/trie/tla/cfg/pb_wit.cfg | 5 + formal/trie/tla/cfg/pbg_exc.cfg | 5 + formal/trie/tla/cfg/pbg_fixed.cfg | 5 + formal/trie/tla/cfg/pbg_rs.cfg | 5 + formal/trie/tla/cfg/pbg_rs_fb.cfg | 5 + formal/trie/tla/cfg/pbg_rs_fbA.cfg | 5 + formal/trie/tla/cfg/pbg_rs_fix.cfg | 5 + formal/trie/tla/cfg/tq2_ref.cfg | 5 + formal/trie/tla/cfg/tq2_star.cfg | 5 + formal/trie/tla/cfg/tq_exact.cfg | 5 + formal/trie/tla/cfg/tq_fixed.cfg | 5 + formal/trie/tla/cfg/tq_fixed5.cfg | 6 + formal/trie/tla/cfg/tq_fixed_ref.cfg | 5 + formal/trie/tla/cfg/tq_nontop.cfg | 5 + formal/trie/tla/cfg/tq_plant.cfg | 5 + formal/trie/tla/cfg/tq_ref.cfg | 5 + formal/trie/tla/cfg/tq_refspec.cfg | 5 + formal/trie/tla/cfg/tq_spec.cfg | 5 + formal/trie/tla/cfg/tq_star.cfg | 5 + formal/trie/tla/cfg/tq_sup.cfg | 5 + formal/trie/tla/cfg/tq_wit.cfg | 5 + formal/trie/tla/expected.txt | 44 ++ formal/trie/tla/run.sh | 6 + formal/trie/tla/runall.sh | 58 ++ 311 files changed, 16967 insertions(+) create mode 100644 formal/.gitignore create mode 100644 formal/binary-storage/lean/BinaryStorage.lean create mode 100644 formal/binary-storage/lean/BinaryStorage/Check.lean create mode 100644 formal/binary-storage/lean/BinaryStorage/Model.lean create mode 100644 formal/binary-storage/lean/BinaryStorage/Proof.lean create mode 100644 formal/binary-storage/lean/BinaryStorage/Results.lean create mode 100644 formal/binary-storage/lean/NOTES.md create mode 100644 formal/binary-storage/lean/lake-manifest.json create mode 100644 formal/binary-storage/lean/lakefile.toml create mode 100644 formal/binary-storage/lean/lean-toolchain create mode 100644 formal/binary-storage/lean/theorems.txt create mode 100644 formal/binary-storage/tla/BinaryStorage.tla create mode 100644 formal/binary-storage/tla/MC.tla create mode 100644 formal/binary-storage/tla/NOTES.md create mode 100644 formal/binary-storage/tla/cfg/ablateA.cfg create mode 100644 formal/binary-storage/tla/cfg/ablateB.cfg create mode 100644 formal/binary-storage/tla/cfg/ablateC.cfg create mode 100644 formal/binary-storage/tla/cfg/ablateD.cfg create mode 100644 formal/binary-storage/tla/cfg/fixed_L.cfg create mode 100644 formal/binary-storage/tla/cfg/fixed_L2.cfg create mode 100644 formal/binary-storage/tla/cfg/fixed_M.cfg create mode 100644 formal/binary-storage/tla/cfg/fixed_M2.cfg create mode 100644 formal/binary-storage/tla/cfg/fixed_R.cfg create mode 100644 formal/binary-storage/tla/cfg/fixed_S.cfg create mode 100644 formal/binary-storage/tla/cfg/happy_LoaderNoPartialRead.cfg create mode 100644 formal/binary-storage/tla/cfg/happy_MainNoPartialRead.cfg create mode 100644 formal/binary-storage/tla/cfg/happy_NoDetachedStore.cfg create mode 100644 formal/binary-storage/tla/cfg/happy_NoStaleRead.cfg create mode 100644 formal/binary-storage/tla/cfg/happy_NotSourceOnlyWhenStored.cfg create mode 100644 formal/binary-storage/tla/cfg/happy_SetThreadSafe.cfg create mode 100644 formal/binary-storage/tla/cfg/orig_LoaderNoPartialRead.cfg create mode 100644 formal/binary-storage/tla/cfg/orig_MainNoPartialRead.cfg create mode 100644 formal/binary-storage/tla/cfg/orig_NoDetachedStore.cfg create mode 100644 formal/binary-storage/tla/cfg/orig_NoStaleRead.cfg create mode 100644 formal/binary-storage/tla/cfg/orig_NotSourceOnlyWhenStored.cfg create mode 100644 formal/binary-storage/tla/cfg/orig_P1_nofail.cfg create mode 100644 formal/binary-storage/tla/cfg/orig_SetThreadSafe.cfg create mode 100644 formal/binary-storage/tla/cfg/orig_StoresAccounted.cfg create mode 100644 formal/binary-storage/tla/cfg/orig_TypeOK.cfg create mode 100644 formal/binary-storage/tla/cfg/orig_adr.cfg create mode 100644 formal/binary-storage/tla/cfg/orig_detached_nolinkfail.cfg create mode 100644 formal/binary-storage/tla/cfg/orig_live.cfg create mode 100644 formal/binary-storage/tla/cfg/orig_live_M.cfg create mode 100644 formal/binary-storage/tla/cfg/orig_loaderpartial_M.cfg create mode 100644 formal/binary-storage/tla/cfg/orig_mainpartial.cfg create mode 100644 formal/binary-storage/tla/cfg/orig_rdw.cfg create mode 100644 formal/binary-storage/tla/cfg/orig_stale_nofail.cfg create mode 100644 formal/binary-storage/tla/cfg/planted.cfg create mode 100644 formal/binary-storage/tla/cfg/smoke.cfg create mode 100644 formal/binary-storage/tla/cfg/wit_fixed_WitnessCallerRuns.cfg create mode 100644 formal/binary-storage/tla/cfg/wit_fixed_WitnessDone.cfg create mode 100644 formal/binary-storage/tla/cfg/wit_fixed_WitnessGoodRead.cfg create mode 100644 formal/binary-storage/tla/cfg/wit_fixed_WitnessSecondClust.cfg create mode 100644 formal/binary-storage/tla/cfg/wit_fixed_WitnessStoreOk.cfg create mode 100644 formal/binary-storage/tla/cfg/wit_fixed_WitnessTimeout.cfg create mode 100644 formal/binary-storage/tla/cfg/wit_orig_WitnessCallerRuns.cfg create mode 100644 formal/binary-storage/tla/cfg/wit_orig_WitnessDone.cfg create mode 100644 formal/binary-storage/tla/cfg/wit_orig_WitnessGoodRead.cfg create mode 100644 formal/binary-storage/tla/cfg/wit_orig_WitnessSecondClust.cfg create mode 100644 formal/binary-storage/tla/cfg/wit_orig_WitnessStoreOk.cfg create mode 100644 formal/binary-storage/tla/cfg/wit_orig_WitnessTimeout.cfg create mode 100755 formal/binary-storage/tla/check_all.sh create mode 100644 formal/binary-storage/tla/expected.txt create mode 100755 formal/binary-storage/tla/gen.sh create mode 100755 formal/binary-storage/tla/run.sh create mode 100755 formal/binary-storage/tla/trace.py create mode 100755 formal/check.sh create mode 100644 formal/find-refs/lean/.gitignore create mode 100644 formal/find-refs/lean/FindRefs.lean create mode 100644 formal/find-refs/lean/FindRefs/Buggy.lean create mode 100644 formal/find-refs/lean/FindRefs/Check.lean create mode 100644 formal/find-refs/lean/FindRefs/Fixed.lean create mode 100644 formal/find-refs/lean/FindRefs/Proof.lean create mode 100644 formal/find-refs/lean/FindRefs/State.lean create mode 100644 formal/find-refs/lean/FindRefs/Theorems.lean create mode 100644 formal/find-refs/lean/NOTES.md create mode 100644 formal/find-refs/lean/Report.lean create mode 100644 formal/find-refs/lean/lake-manifest.json create mode 100644 formal/find-refs/lean/lakefile.toml create mode 100644 formal/find-refs/lean/lean-toolchain create mode 100644 formal/find-refs/lean/report.txt create mode 100644 formal/find-refs/lean/theorems.txt create mode 100644 formal/find-refs/tla/FindRefs.cfg create mode 100644 formal/find-refs/tla/FindRefs.tla create mode 100644 formal/find-refs/tla/FindRefsFixed.cfg create mode 100644 formal/find-refs/tla/NOTES.md create mode 100755 formal/find-refs/tla/coverage.sh create mode 100644 formal/find-refs/tla/expected.txt create mode 100755 formal/find-refs/tla/matrix.sh create mode 100755 formal/find-refs/tla/run.sh create mode 100644 formal/find-refs/tla/trace.py create mode 100644 formal/find-refs/tla/traces/fixed_minus_plock_OneRootCreated.txt create mode 100644 formal/find-refs/tla/traces/fixed_minus_plock_with_atomic_NoStale.txt create mode 100644 formal/find-refs/tla/traces/orig_NoCME.txt create mode 100644 formal/find-refs/tla/traces/orig_NoDeadlock.txt create mode 100644 formal/find-refs/tla/traces/orig_NoDupRef.txt create mode 100644 formal/find-refs/tla/traces/orig_NoForeign.txt create mode 100644 formal/find-refs/tla/traces/orig_NoLostRef.txt create mode 100644 formal/find-refs/tla/traces/orig_NoLostRoot.txt create mode 100644 formal/find-refs/tla/traces/orig_OneRootCreated.txt create mode 100644 formal/find-refs/tla/traces/orig_flagfixed_lost_ref_via_duplicate_root.txt create mode 100644 formal/find-refs/tla/traces/planted.txt create mode 100644 formal/parallel-loader/lean/.gitignore create mode 100644 formal/parallel-loader/lean/NOTES.md create mode 100644 formal/parallel-loader/lean/ParallelLoader.lean create mode 100644 formal/parallel-loader/lean/ParallelLoader/Check.lean create mode 100644 formal/parallel-loader/lean/ParallelLoader/Model.lean create mode 100644 formal/parallel-loader/lean/ParallelLoader/Proof.lean create mode 100644 formal/parallel-loader/lean/ParallelLoader/Results.lean create mode 100644 formal/parallel-loader/lean/lake-manifest.json create mode 100644 formal/parallel-loader/lean/lakefile.toml create mode 100644 formal/parallel-loader/lean/lean-toolchain create mode 100644 formal/parallel-loader/lean/theorems.txt create mode 100644 formal/parallel-loader/tla/NOTES.md create mode 100644 formal/parallel-loader/tla/ParallelLoader.cfg create mode 100644 formal/parallel-loader/tla/ParallelLoader.tla create mode 100644 formal/parallel-loader/tla/ParallelLoaderFixed.tla create mode 100644 formal/parallel-loader/tla/cfg/abort_arr1.cfg create mode 100644 formal/parallel-loader/tla/cfg/abort_sync.cfg create mode 100644 formal/parallel-loader/tla/cfg/abort_unb.cfg create mode 100644 formal/parallel-loader/tla/cfg/big_AbortOnlyOnCancel.cfg create mode 100644 formal/parallel-loader/tla/cfg/big_Bookkeeping.cfg create mode 100644 formal/parallel-loader/tla/cfg/bk_arr1.cfg create mode 100644 formal/parallel-loader/tla/cfg/bk_sync.cfg create mode 100644 formal/parallel-loader/tla/cfg/bk_unb.cfg create mode 100644 formal/parallel-loader/tla/cfg/full_l_arr2.cfg create mode 100644 formal/parallel-loader/tla/cfg/full_l_sync.cfg create mode 100644 formal/parallel-loader/tla/cfg/full_l_unb.cfg create mode 100644 formal/parallel-loader/tla/cfg/full_m_arr1.cfg create mode 100644 formal/parallel-loader/tla/cfg/full_m_sync.cfg create mode 100644 formal/parallel-loader/tla/cfg/full_m_unb.cfg create mode 100644 formal/parallel-loader/tla/cfg/full_s_arr1.cfg create mode 100644 formal/parallel-loader/tla/cfg/full_s_sync.cfg create mode 100644 formal/parallel-loader/tla/cfg/full_s_unb.cfg create mode 100644 formal/parallel-loader/tla/cfg/full_xl_arr2.cfg create mode 100644 formal/parallel-loader/tla/cfg/leak_arr1.cfg create mode 100644 formal/parallel-loader/tla/cfg/live_done_arr1.cfg create mode 100644 formal/parallel-loader/tla/cfg/live_done_sync.cfg create mode 100644 formal/parallel-loader/tla/cfg/live_done_unb.cfg create mode 100644 formal/parallel-loader/tla/cfg/live_int_arr1.cfg create mode 100644 formal/parallel-loader/tla/cfg/live_int_sync.cfg create mode 100644 formal/parallel-loader/tla/cfg/live_int_unb.cfg create mode 100644 formal/parallel-loader/tla/cfg/live_noint_arr1.cfg create mode 100644 formal/parallel-loader/tla/cfg/live_noint_sync.cfg create mode 100644 formal/parallel-loader/tla/cfg/live_noint_unb.cfg create mode 100644 formal/parallel-loader/tla/cfg/live_swallow_arr1.cfg create mode 100644 formal/parallel-loader/tla/cfg/live_swallow_sync.cfg create mode 100644 formal/parallel-loader/tla/cfg/live_swallow_unb.cfg create mode 100644 formal/parallel-loader/tla/cfg/planted_abort.cfg create mode 100644 formal/parallel-loader/tla/cfg/qc_arr1.cfg create mode 100644 formal/parallel-loader/tla/cfg/qc_sync.cfg create mode 100644 formal/parallel-loader/tla/cfg/qc_unb.cfg create mode 100644 formal/parallel-loader/tla/cfg/wit_m_sync.cfg create mode 100755 formal/parallel-loader/tla/check_all.sh create mode 100644 formal/parallel-loader/tla/expected.txt create mode 100755 formal/parallel-loader/tla/gen.sh create mode 100755 formal/parallel-loader/tla/run.sh create mode 100755 formal/parallel-loader/tla/trace.sh create mode 100644 formal/parallel-loader/tla/variants/AblateFix1.tla create mode 100644 formal/parallel-loader/tla/variants/AblateFix2.tla create mode 100644 formal/parallel-loader/tla/variants/AblateFix3.tla create mode 100644 formal/parallel-loader/tla/variants/ParallelLoaderPlanted.tla create mode 100644 formal/pipeline/lean/.gitignore create mode 100644 formal/pipeline/lean/NOTES.md create mode 100644 formal/pipeline/lean/Pipeline.lean create mode 100644 formal/pipeline/lean/Pipeline/Check.lean create mode 100644 formal/pipeline/lean/Pipeline/Configs.lean create mode 100644 formal/pipeline/lean/Pipeline/Model.lean create mode 100644 formal/pipeline/lean/Report.lean create mode 100644 formal/pipeline/lean/Results.lean create mode 100644 formal/pipeline/lean/lake-manifest.json create mode 100644 formal/pipeline/lean/lakefile.toml create mode 100644 formal/pipeline/lean/lean-toolchain create mode 100644 formal/pipeline/lean/report.txt create mode 100644 formal/pipeline/lean/theorems.txt create mode 100644 formal/pipeline/tla/NOTES.md create mode 100644 formal/pipeline/tla/Pipeline.tla create mode 100644 formal/pipeline/tla/cfg/asis_IndexNoDangling.cfg create mode 100644 formal/pipeline/tla/cfg/asis_LatestExists.cfg create mode 100644 formal/pipeline/tla/cfg/asis_LatestFromMaster.cfg create mode 100644 formal/pipeline/tla/cfg/asis_MaintOnOwnLine.cfg create mode 100644 formal/pipeline/tla/cfg/asis_NoCrossRefCancel.cfg create mode 100644 formal/pipeline/tla/cfg/asis_NoLostContent.cfg create mode 100644 formal/pipeline/tla/cfg/asis_OwnLineVersion.cfg create mode 100644 formal/pipeline/tla/cfg/asis_RelLatestIsMax.cfg create mode 100644 formal/pipeline/tla/cfg/asis_RerunProgress.cfg create mode 100644 formal/pipeline/tla/cfg/asis_TagHasRepo.cfg create mode 100644 formal/pipeline/tla/cfg/asis_TagHasRepoOrLive.cfg create mode 100644 formal/pipeline/tla/cfg/asis_W_Evicted.cfg create mode 100644 formal/pipeline/tla/cfg/asis_W_MaintRelease.cfg create mode 100644 formal/pipeline/tla/cfg/asis_W_MasterRelease.cfg create mode 100644 formal/pipeline/tla/cfg/asis_live_maint.cfg create mode 100644 formal/pipeline/tla/cfg/asis_live_master.cfg create mode 100644 formal/pipeline/tla/cfg/asis_live_tags.cfg create mode 100644 formal/pipeline/tla/cfg/fix_MaintOnOwnLine.cfg create mode 100644 formal/pipeline/tla/cfg/fix_W_CalmGoal_maint.cfg create mode 100644 formal/pipeline/tla/cfg/fix_W_Evicted.cfg create mode 100644 formal/pipeline/tla/cfg/fix_W_MaintRelease.cfg create mode 100644 formal/pipeline/tla/cfg/fix_W_MasterRelease.cfg create mode 100644 formal/pipeline/tla/cfg/fix_live_maint.cfg create mode 100644 formal/pipeline/tla/cfg/fix_live_master.cfg create mode 100644 formal/pipeline/tla/cfg/fix_relLatest_ctrl.cfg create mode 100644 formal/pipeline/tla/cfg/fix_safety.cfg create mode 100644 formal/pipeline/tla/cfg/fix_safety_d3.cfg create mode 100644 formal/pipeline/tla/cfg/fix_safety_maint.cfg create mode 100644 formal/pipeline/tla/cfg/fix_safety_wide.cfg create mode 100644 formal/pipeline/tla/cfg/plant_cleanup.cfg create mode 100644 formal/pipeline/tla/cfg/plant_relLatest.cfg create mode 100644 formal/pipeline/tla/expected.txt create mode 100755 formal/pipeline/tla/run.sh create mode 100755 formal/pipeline/tla/run_all.sh create mode 100644 formal/pipeline/tla/trace.py create mode 100644 formal/readonly/comparator/MinSize.java create mode 100644 formal/readonly/comparator/Runner.java create mode 100755 formal/readonly/orphans/check-test-reachability.sh create mode 100644 formal/readonly/orphans/expected.txt create mode 100755 formal/readonly/orphans/selftest.sh create mode 100644 formal/trie/lean/.gitignore create mode 100644 formal/trie/lean/Main.lean create mode 100644 formal/trie/lean/NOTES.md create mode 100644 formal/trie/lean/Trie.lean create mode 100644 formal/trie/lean/Trie/Axioms.lean create mode 100644 formal/trie/lean/Trie/Basic.lean create mode 100644 formal/trie/lean/Trie/Checks.lean create mode 100644 formal/trie/lean/Trie/Consumer.lean create mode 100644 formal/trie/lean/Trie/Domains.lean create mode 100644 formal/trie/lean/Trie/Fixed.lean create mode 100644 formal/trie/lean/Trie/Pattern.lean create mode 100644 formal/trie/lean/Trie/Theorems.lean create mode 100644 formal/trie/lean/Trie/Tree.lean create mode 100644 formal/trie/lean/Trie/TreeSet.lean create mode 100644 formal/trie/lean/Trie/Validate.lean create mode 100644 formal/trie/lean/java-check/RunTests.java create mode 100644 formal/trie/lean/java-check/TrieRepro.java create mode 100644 formal/trie/lean/java-check/fixed-src/com/avaloq/tools/ddk/xtext/naming/QualifiedNamePattern.java create mode 100644 formal/trie/lean/java-check/fixed-src/com/avaloq/tools/ddk/xtext/naming/QualifiedNameSegmentTreeLookup.java create mode 100644 formal/trie/lean/java-check/fixed-src/com/avaloq/tools/ddk/xtext/resource/PatternAwareEObjectDescriptionLookUp.java create mode 100644 formal/trie/lean/lake-manifest.json create mode 100644 formal/trie/lean/lakefile.toml create mode 100644 formal/trie/lean/lean-toolchain create mode 100644 formal/trie/lean/results/axioms.txt create mode 100644 formal/trie/lean/results/formal-test-as-written.txt create mode 100644 formal/trie/lean/results/full-run.txt create mode 100644 formal/trie/lean/results/java-repro.txt create mode 100644 formal/trie/lean/results/junit-as-written-vs-fixed.txt create mode 100644 formal/trie/lean/theorems.txt create mode 100644 formal/trie/tla/Consumer.tla create mode 100644 formal/trie/tla/MC_Cons.tla create mode 100644 formal/trie/tla/MC_Ops.tla create mode 100644 formal/trie/tla/MC_TQ.tla create mode 100644 formal/trie/tla/MC_TQ2.tla create mode 100644 formal/trie/tla/NOTES.md create mode 100644 formal/trie/tla/PatternBounds.tla create mode 100644 formal/trie/tla/QNBase.tla create mode 100644 formal/trie/tla/TrieCore.tla create mode 100644 formal/trie/tla/TrieOps.tla create mode 100644 formal/trie/tla/TrieQuery.tla create mode 100644 formal/trie/tla/cfg/co_ci.cfg create mode 100644 formal/trie/tla/cfg/co_ci_fb.cfg create mode 100644 formal/trie/tla/cfg/co_cs.cfg create mode 100644 formal/trie/tla/cfg/co_cs_fb.cfg create mode 100644 formal/trie/tla/cfg/co_fixed.cfg create mode 100644 formal/trie/tla/cfg/co_wit.cfg create mode 100644 formal/trie/tla/cfg/op_bagns.cfg create mode 100644 formal/trie/tla/cfg/op_copy.cfg create mode 100644 formal/trie/tla/cfg/op_exact.cfg create mode 100644 formal/trie/tla/cfg/op_exactref.cfg create mode 100644 formal/trie/tla/cfg/op_fixed.cfg create mode 100644 formal/trie/tla/cfg/op_fixed5.cfg create mode 100644 formal/trie/tla/cfg/op_fixed_sh.cfg create mode 100644 formal/trie/tla/cfg/op_fixed_sh5.cfg create mode 100644 formal/trie/tla/cfg/op_map.cfg create mode 100644 formal/trie/tla/cfg/op_nodup.cfg create mode 100644 formal/trie/tla/cfg/op_plant.cfg create mode 100644 formal/trie/tla/cfg/op_share.cfg create mode 100644 formal/trie/tla/cfg/op_sizespec.cfg create mode 100644 formal/trie/tla/cfg/op_sizetree.cfg create mode 100644 formal/trie/tla/cfg/op_wit1.cfg create mode 100644 formal/trie/tla/cfg/op_wit2.cfg create mode 100644 formal/trie/tla/cfg/pb_cnt.cfg create mode 100644 formal/trie/tla/cfg/pb_cnt1.cfg create mode 100644 formal/trie/tla/cfg/pb_fixed.cfg create mode 100644 formal/trie/tla/cfg/pb_ord.cfg create mode 100644 formal/trie/tla/cfg/pb_plant.cfg create mode 100644 formal/trie/tla/cfg/pb_rs.cfg create mode 100644 formal/trie/tla/cfg/pb_rs2.cfg create mode 100644 formal/trie/tla/cfg/pb_ts.cfg create mode 100644 formal/trie/tla/cfg/pb_wit.cfg create mode 100644 formal/trie/tla/cfg/pbg_exc.cfg create mode 100644 formal/trie/tla/cfg/pbg_fixed.cfg create mode 100644 formal/trie/tla/cfg/pbg_rs.cfg create mode 100644 formal/trie/tla/cfg/pbg_rs_fb.cfg create mode 100644 formal/trie/tla/cfg/pbg_rs_fbA.cfg create mode 100644 formal/trie/tla/cfg/pbg_rs_fix.cfg create mode 100644 formal/trie/tla/cfg/tq2_ref.cfg create mode 100644 formal/trie/tla/cfg/tq2_star.cfg create mode 100644 formal/trie/tla/cfg/tq_exact.cfg create mode 100644 formal/trie/tla/cfg/tq_fixed.cfg create mode 100644 formal/trie/tla/cfg/tq_fixed5.cfg create mode 100644 formal/trie/tla/cfg/tq_fixed_ref.cfg create mode 100644 formal/trie/tla/cfg/tq_nontop.cfg create mode 100644 formal/trie/tla/cfg/tq_plant.cfg create mode 100644 formal/trie/tla/cfg/tq_ref.cfg create mode 100644 formal/trie/tla/cfg/tq_refspec.cfg create mode 100644 formal/trie/tla/cfg/tq_spec.cfg create mode 100644 formal/trie/tla/cfg/tq_star.cfg create mode 100644 formal/trie/tla/cfg/tq_sup.cfg create mode 100644 formal/trie/tla/cfg/tq_wit.cfg create mode 100644 formal/trie/tla/expected.txt create mode 100755 formal/trie/tla/run.sh create mode 100755 formal/trie/tla/runall.sh diff --git a/formal/.gitignore b/formal/.gitignore new file mode 100644 index 000000000..dea2a48c1 --- /dev/null +++ b/formal/.gitignore @@ -0,0 +1,27 @@ +# Tools fetched locally and harness output. +.tools/ +.check/ + +# Lean build output. +**/.lake/ + +# TLC state and metadirs. +**/states/ +**/meta/ +**/meta-*/ + +# Logs and generated run artefacts of the model-checking scripts. +*.log +*.out +**/tla/runs/ +**/tla/out/ +**/tla/logs/ + +# Compiled Java of the cross-checks. +**/java-check/out/ +**/java-check/out-fixed/ +readonly/comparator/out/ + +# Machine-specific classpaths and third-party source extracts +**/classpath*.txt +find-refs/.src/ diff --git a/formal/binary-storage/lean/BinaryStorage.lean b/formal/binary-storage/lean/BinaryStorage.lean new file mode 100644 index 000000000..0ef413929 --- /dev/null +++ b/formal/binary-storage/lean/BinaryStorage.lean @@ -0,0 +1,4 @@ +import BinaryStorage.Model +import BinaryStorage.Check +import BinaryStorage.Results +import BinaryStorage.Proof diff --git a/formal/binary-storage/lean/BinaryStorage/Check.lean b/formal/binary-storage/lean/BinaryStorage/Check.lean new file mode 100644 index 000000000..cfbb5d38e --- /dev/null +++ b/formal/binary-storage/lean/BinaryStorage/Check.lean @@ -0,0 +1,103 @@ +import Std.Data.HashMap +import BinaryStorage.Model + +namespace BinaryStorage +open Std + +/-- Explored graph in BFS order: the parent chain of a state is a shortest path from `init`. -/ +structure Graph where + states : Array St := #[] + parent : Array (Option (Nat × Act)) := #[] + edges : Array (List Nat) := #[] + index : HashMap St Nat := {} + complete : Bool := true + +/-- Exhaustive BFS to a fixpoint (fuel only keeps the definition total). -/ +def explore (c : Cfg) (fuel : Nat := 5000000) : Graph := Id.run do + let s0 := init c + let mut g : Graph := { states := #[s0], parent := #[none], edges := #[[]], + index := ({} : HashMap St Nat).insert s0 0 } + let mut head := 0 + for _ in [0:fuel] do + if h : head < g.states.size then + let s := g.states[head] + let mut out : List Nat := [] + for (a, t) in succ c s do + match g.index.get? t with + | some j => out := j :: out + | none => + let j := g.states.size + g := { g with states := g.states.push t, parent := g.parent.push (some (head, a)), + edges := g.edges.push [], index := g.index.insert t j } + out := j :: out + g := { g with edges := g.edges.set! head out } + head := head + 1 + else break + if head < g.states.size then g := { g with complete := false } + return g + +def Graph.trace (g : Graph) (i : Nat) : List Act := Id.run do + let mut acc : List Act := [] + let mut k := i + for _ in [0:g.states.size] do + match g.parent[k]! with + | some (p, a) => acc := a :: acc; k := p + | none => break + return acc + +def Graph.firstViolation (g : Graph) (p : St → Bool) : Option Nat := + (List.range g.states.size).find? fun i => !p g.states[i]! + +/-- Kahn's algorithm: true iff the reachable graph is acyclic (every run is finite). -/ +def Graph.acyclic (g : Graph) : Bool := Id.run do + let n := g.states.size + let mut indeg : Array Nat := Array.replicate n 0 + for es in g.edges do + for j in es do indeg := indeg.modify j (· + 1) + let mut stack : List Nat := (List.range n).filter (indeg[·]! == 0) + let mut seen := 0 + for _ in [0:n] do + match stack with + | [] => break + | i :: rest => + stack := rest; seen := seen + 1 + for j in g.edges[i]! do + indeg := indeg.modify j (· - 1) + if indeg[j]! == 0 then stack := j :: stack + return seen == n + +/-- Non-terminal states without successors. -/ +def Graph.deadlocks (c : Cfg) (g : Graph) : Nat := + ((List.range g.states.size).filter fun i => g.edges[i]!.isEmpty && !terminal c g.states[i]!).length + +structure Report where + states : Nat + complete : Bool + acyclic : Bool + deadlocks : Nat + p1 : Option Nat + p2 : Option Nat + p3partial : Option Nat + p3stale : Option Nat + p4 : Option Nat + pEnd : Option Nat + deriving Repr + +def report (c : Cfg) : Report := + let g := explore c + let fv (p : St → Bool) : Option Nat := (g.firstViolation p).map fun i => (g.trace i).length + { states := g.states.size, complete := g.complete, acyclic := g.acyclic, deadlocks := g.deadlocks c, + p1 := fv p1, p2 := fv (p2 c), p3partial := fv p3partial, p3stale := fv p3stale, p4 := fv p4, pEnd := fv (pEnd c) } + +/-- Shortest counterexample (list of actions) for property `p`, if any. -/ +def cex (c : Cfg) (p : St → Bool) : Option (List Act) := + let g := explore c + (g.firstViolation p).map g.trace + +/-- Boolean verdict usable by `native_decide`: all five properties hold. -/ +def allHold (c : Cfg) : Bool := + let r := report c + r.complete && r.acyclic && r.deadlocks == 0 && r.p1.isNone && r.p2.isNone && + r.p3partial.isNone && r.p3stale.isNone && r.p4.isNone && r.pEnd.isNone + +end BinaryStorage diff --git a/formal/binary-storage/lean/BinaryStorage/Model.lean b/formal/binary-storage/lean/BinaryStorage/Model.lean new file mode 100644 index 000000000..a63bf4da5 --- /dev/null +++ b/formal/binary-storage/lean/BinaryStorage/Model.lean @@ -0,0 +1,338 @@ +/-! +Model of the binary-model storage path of `MonitoredClusteringBuilderState` (MCBS) and its +interaction with the cluster loop, the DDK `ParallelResourceLoader` (PRL) threads and the shared +`SourceLevelURICache.sources` set (a plain `java.util.HashSet`, Xtext SourceLevelURICache:14). + +Instance: three URIs, all rebuilt in this build. + a (0), c (1) : cluster 1 (initial queue, installed as sources by installSourceLevelURIs) + b (2) : cluster 2 (affected by a; added to sources by queueAffectedResources MCBS:1296) + b depends on a: main-thread linking of b resolves a; optionally loading b also touches a. + +Threads: main builder thread (tid 0), cluster-1 loader (tid 1), cluster-2 loader (tid 2), +storage workers (tid 10+i), across executor generations (MCBS:871 recreates the pool). +-/ +namespace BinaryStorage + +/-- State of the binary file `.bin` on disk. `stale` = complete but from the previous build. -/ +inductive Bin | none | stale | part | fresh + deriving DecidableEq, Hashable, Repr, Inhabited + +inductive Task | idle | queued | running | done | failed | dropped | discarded + deriving DecidableEq, Hashable, Repr, Inhabited + +/-- Phases of one `doStoreBinaryResource` (MCBS:740-765). -/ +inductive Ph | ser | wr | wrote | rmB + deriving DecidableEq, Hashable, Repr, Inhabited + +structure Job where + u : Nat + ph : Ph + intr : Bool -- interrupted by shutdownNow + deriving DecidableEq, Hashable, Repr, Inhabited + +structure W where + gen : Nat + started : Bool + job : Option Job + deriving DecidableEq, Hashable, Repr, Inhabited + +/-- An in-flight (non-atomic) operation on the shared HashSet. -/ +structure Op where + tid : Nat + wr : Bool + racy : Bool + deriving DecidableEq, Hashable, Repr, Inhabited + +/-- Loader micro-steps: contains() begin/end on the sources set, then publish the result. -/ +inductive LA | chkB (x : Nat) | chkE (x : Nat) | pub (x : Nat) + deriving DecidableEq, Hashable, Repr, Inhabited + +/-- Main-thread program instructions. -/ +inductive I + | next (u : Nat) | store (u : Nat) | rmB (u : Nat) | rmE (u : Nat) + | addB (u : Nat) | addE (u : Nat) | startL2 | shut | awaitT | waitActive | recreate | clear + | resB (u : Nat) | resE (u : Nat) | done + deriving DecidableEq, Hashable, Repr, Inhabited + +def uA : Nat := 0 +def uC : Nat := 1 +def uB : Nat := 2 + +structure Cfg where + nW : Nat := 1 -- BINARY_STORAGE_EXECUTOR_PARALLELISM (scaled down) + qcap : Nat := 1 -- BINARY_STORAGE_EXECUTOR_QUEUE_CAPACITY (scaled down) + timeout : Bool := true -- awaitTermination may time out (1 min) or be interrupted + ioFail : Bool := false -- writeResource may throw IOException (swallowed by Xtext) + touchDep : Bool := true -- loading b in a loader thread may load a into the local set + fixed : Bool := false -- apply the candidate fix + plant : Bool := false -- planted bug (on top of `fixed`): remove from sources before writing + initBin : Bin := .stale -- previous build left a complete binary + raceNondet : Bool := true -- racing HashSet ops may miss a key / lose a write (false: only flag the race) + deriving Repr + +structure St where + pc : Nat + inl : Option Job -- CallerRunsPolicy: main runs the store itself + ops : List Op + inSrc : List Bool + bin : List Bin + task : List Task + rs : List Bool -- resource currently in the main resource set + loaded : List Bool -- loader published the resource + l1 : List LA + l2 : List LA + l2on : Bool + gen : Nat + shut : Bool + queue : List Nat + workers : List W + reported : Nat -- "{} tasks not processed" (MCBS:880) + setRace : Bool + partialLd : Bool + partialMain : Bool + staleLd : Bool + staleMain : Bool + deriving DecidableEq, Hashable, Repr, Inhabited + +abbrev Act := String + +def storeSeq (c : Cfg) (u : Nat) : List I := + if c.fixed then [.next u, .store u] else [.next u, .store u, .rmB u, .rmE u] + +def awaitSeq (c : Cfg) : List I := + if c.fixed then [.shut, .awaitT, .waitActive, .recreate] else [.shut, .awaitT, .recreate] + +/-- Main-thread program, in the order of MCBS.doUpdate L529-690 (bug) or the fixed order. -/ +def prog (c : Cfg) : List I := + let cluster1 := storeSeq c uA ++ storeSeq c uC + let qa : List I := if c.fixed then [.addB uB] else [.addB uB, .addE uB] + let boundary := + if c.fixed then qa ++ awaitSeq c ++ [.clear, .startL2] + else qa ++ [.startL2] ++ awaitSeq c ++ [.clear] + let res : List I := if c.fixed then [.resB uA] else [.resB uA, .resE uA] + let cluster2 := [.next uB] ++ res ++ (storeSeq c uB).drop 1 + cluster1 ++ boundary ++ cluster2 ++ awaitSeq c ++ [.done] + +def loadSeq (c : Cfg) (x : Nat) : List LA := + if c.fixed then [.chkB x] else [.chkB x, .chkE x] + +def init (c : Cfg) : St := + { pc := 0, inl := none, ops := [], + inSrc := [true, true, false], bin := [c.initBin, c.initBin, c.initBin], + task := [.idle, .idle, .idle], rs := [false, false, false], loaded := [false, false, false], + l1 := loadSeq c uA ++ [.pub uA] ++ loadSeq c uC ++ [.pub uC], + l2 := loadSeq c uB ++ (if c.touchDep then loadSeq c uA else []) ++ [.pub uB], + l2on := false, gen := 0, shut := false, queue := [], + workers := (List.range c.nW).map fun _ => { gen := 0, started := false, job := none }, + reported := 0, setRace := false, partialLd := false, partialMain := false, + staleLd := false, staleMain := false } + +/-! ### Shared-set operations (non-atomic unless the fix makes the set concurrent) -/ + +def opBegin (s : St) (tid : Nat) (wr : Bool) : St := + let clash (o : Op) := o.tid != tid && (o.wr || wr) + let conflict := s.ops.any clash + { s with ops := s.ops.map (fun o => if clash o then { o with racy := true } else o) ++ [⟨tid, wr, conflict⟩], + setRace := s.setRace || conflict } + +def opEnd (c : Cfg) (s : St) (tid : Nat) : Bool × St := + match s.ops.find? (·.tid == tid) with + | some o => (o.racy && c.raceNondet, { s with ops := s.ops.filter (·.tid != tid) }) + | none => (false, s) + +/-- Possible results of `contains(x)`; a read racing a structural modification (HashMap resize + installs the new, empty table before transferring) may miss a present key. -/ +def containsRes (s : St) (x : Nat) (racy : Bool) : List Bool := + if racy then (if s.inSrc[x]! then [true, false] else [false]) else [s.inSrc[x]!] + +/-- Possible results of a write to the set: a racing write may be lost. -/ +def writeRes (s : St) (x : Nat) (v : Bool) (racy : Bool) : List St := + let applied := { s with inSrc := s.inSrc.set x v } + if racy && s.inSrc[x]! != v then [applied, s] else [applied] + +/-- A load of `x` after `shouldLoadFromStorage` answered "is source" = `res` + (ResourceStorageFacade:49-54 -> StorageAwareResource:82-88). -/ +def readOutcome (s : St) (x : Nat) (isMain : Bool) (res : Bool) : St := + if res then s else + match s.bin[x]! with + | .part => if isMain then { s with partialMain := true } else { s with partialLd := true } + | .stale => if isMain then { s with staleMain := true } else { s with staleLd := true } + | _ => s + +def setTask (s : St) (u : Nat) (t : Task) : St := { s with task := s.task.set u t } +def setBin (s : St) (u : Nat) (b : Bin) : St := { s with bin := s.bin.set u b } + +/-! ### One storage job (`doStoreBinaryResource`) executed by thread `tid` -/ + +def jobSteps (c : Cfg) (s : St) (tid : Nat) (j : Job) : List (Act × St × Option Job) := + let u := j.u + match j.ph with + | .ser => + if !s.rs[u]! then + [("store: resource detached, save throws -> deleteStorage (DLRSF:77-79, MCBS:765)", + setTask (setBin s u .none) u .failed, none)] + else if c.plant then + [("PLANTED: sources.remove before write", setBin { s with inSrc := s.inSrc.set u false } u .part, + some { j with ph := .wr })] + else + [("store: generateFile starts writing binary (ResourceStorageFacade:104)", setBin s u .part, + some { j with ph := .wr })] ++ + (if c.ioFail then + (if c.fixed then [("store: IOException, fixed: delete storage, keep in sources", setTask (setBin s u .none) u .failed, none)] + else [("store: writeResource IOException swallowed, old binary kept (ResourceStorageFacade:97-103)", s, + some { j with ph := .wrote })]) + else []) + | .wr => + [("store: generateFile completes", setBin s u .fresh, some { j with ph := .wrote })] ++ + (if j.intr then [("store: interrupted write fails -> deleteStorage (DLRSF:77-79)", + setTask (setBin s u .none) u .failed, none)] else []) + | .wrote => + if c.plant then [("store done", setTask s u .done, none)] + else if c.fixed then + [("store: sources.remove after complete write (concurrent set)", + setTask { s with inSrc := s.inSrc.set u false } u .done, none)] + else [("store: sources.remove begins (MCBS:754)", opBegin s tid true, some { j with ph := .rmB })] + | .rmB => + let (racy, s') := opEnd c s tid + (writeRes s' u false racy).map fun t => ("store: sources.remove ends (MCBS:754)", setTask t u .done, none) + +/-! ### Successor function -/ + +def mainSteps (c : Cfg) (s : St) : List (Act × St) := + match s.inl with + | some j => + (jobSteps c s 0 j).map fun (a, t, j') => ("main(CallerRuns) " ++ a, { t with inl := j' }) + | none => + let p := prog c + let adv (t : St) : St := { t with pc := t.pc + 1 } + match p[s.pc]? with + | none => [] + | some ins => + match ins with + | .done => [] + | .next u => + if s.loaded[u]! then [("main: loadOperation.next(), addResource (MCBS:537)", adv { s with rs := s.rs.set u true })] + else [] + | .store u => + let s := adv s + if s.shut then [("main: execute on shut-down pool, CallerRuns discards silently (MCBS:726)", setTask s u .discarded)] + else match s.workers.findIdx? (fun w => w.gen == s.gen && !w.started) with + | some i => + [("main: execute -> new core worker (MCBS:726)", + setTask { s with workers := s.workers.set i { gen := s.gen, started := true, job := some ⟨u, .ser, false⟩ } } u .running)] + | none => + if s.queue.length < c.qcap then + [("main: execute -> queued (MCBS:726)", setTask { s with queue := s.queue ++ [u] } u .queued)] + else + [("main: queue full, CallerRunsPolicy runs store inline (MCBS:726)", + setTask { s with inl := some ⟨u, .ser, false⟩ } u .running)] + | .rmB _ => [("main: sources.remove(changedURI) begins (MCBS:656)", adv (opBegin s 0 true))] + | .rmE u => + let (racy, s') := opEnd c s 0 + (writeRes s' u false racy).map fun t => ("main: sources.remove(changedURI) ends (MCBS:656)", adv t) + | .addB u => + if c.fixed then [("main: queueAffectedResources sources.add (concurrent set)", adv { s with inSrc := s.inSrc.set u true })] + else [("main: queueAffectedResources sources.add begins (MCBS:1296)", adv (opBegin s 0 true))] + | .addE u => + let (racy, s') := opEnd c s 0 + (writeRes s' u true racy).map fun t => ("main: queueAffectedResources sources.add ends (MCBS:1296)", adv t) + | .startL2 => [("main: next cluster loadOperation.load(queue) starts loaders (MCBS:668-669)", adv { s with l2on := true })] + | .shut => [("main: binaryStorageExecutor.shutdown() (MCBS:826)", adv { s with shut := true })] + | .awaitT => + let cur := s.workers.filter (·.gen == s.gen) + let terminated := s.queue.isEmpty && cur.all (·.job.isNone) + if terminated then [("main: awaitTermination -> true (MCBS:837)", adv s)] + else if c.timeout then + -- fix (d): the not-processed stores' outdated binaries are deleted + let s1 := s.queue.foldl (fun t u => let t := setTask t u .dropped; if c.fixed then setBin t u .none else t) s + [("main: awaitTermination times out/interrupted -> shutdownNow (MCBS:837,856,879)", + adv { s1 with queue := [], reported := s.reported + s.queue.length, + workers := s.workers.map fun (w : W) => + if w.gen == s.gen then { w with job := w.job.map fun j => { j with intr := true } } else w })] + else [] + | .waitActive => + if (s.workers.filter (·.gen == s.gen)).all (·.job.isNone) then [("main(fixed): wait for active stores", adv s)] else [] + | .recreate => + [("main: binaryStorageExecutor = makeBinaryStorageExecutor() (MCBS:871)", + adv { s with gen := s.gen + 1, shut := false, + workers := s.workers ++ (List.range c.nW).map fun _ => { gen := s.gen + 1, started := false, job := none } })] + | .clear => [("main: clearResourceSet clears resource set (MCBS:1207)", adv { s with rs := [false, false, false] })] + | .resB x => + if s.rs[x]! then [("main: dependency already in resource set", { s with pc := s.pc + (if c.fixed then 1 else 2) })] + else if c.fixed then + [("main: resolve dependency -> getResource(load=true), shouldLoadFromStorage", + adv (readOutcome { s with rs := s.rs.set x true } x true s.inSrc[x]!))] + else [("main: resolveLazyCrossReferences loads dependency; shouldLoadFromStorage contains() begins (MCBS:564, RSF:51)", + adv (opBegin s 0 false))] + | .resE x => + let (racy, s') := opEnd c s 0 + (containsRes s' x racy).map fun r => + ("main: contains() ends -> " ++ (if r then "parse source" else "load binary (StorageAwareResource:86)"), + adv (readOutcome { s' with rs := s'.rs.set x true } x true r)) + +def loaderSteps (c : Cfg) (s : St) (tid : Nat) (l : List LA) (upd : St → List LA → St) : List (Act × St) := + let name := if tid == 1 then "loader1: " else "loader2: " + match l with + | [] => [] + | a :: rest => + match a with + | .pub x => [(name ++ "publish loaded resource (PRL:323)", upd { s with loaded := s.loaded.set x true } rest)] + | .chkB x => + if c.fixed then [(name ++ "load, shouldLoadFromStorage (concurrent set)", upd (readOutcome s x false s.inSrc[x]!) rest)] + else [(name ++ s!"load uri#{x}: shouldLoadFromStorage contains() begins (PRL:174, RSF:51)", upd (opBegin s tid false) rest)] + | .chkE x => + let (racy, s') := opEnd c s tid + (containsRes s' x racy).map fun r => + (name ++ s!"contains(uri#{x}) ends -> " ++ (if r then "parse source" else "load binary"), + upd (readOutcome s' x false r) rest) + +def workerSteps (c : Cfg) (s : St) : List (Act × St) := Id.run do + let mut out : List (Act × St) := [] + for i in [0:s.workers.length] do + let w := s.workers[i]! + match w.job with + | some j => + for (a, t, j') in jobSteps c s (10 + i) j do + out := (s!"worker{i}(gen{w.gen}): " ++ a, { t with workers := t.workers.set i { w with job := j' } }) :: out + | none => + if w.gen == s.gen && w.started then + match s.queue with + | u :: q => + out := (s!"worker{i}: takes store of uri#{u} from queue", + setTask { s with queue := q, workers := s.workers.set i { w with job := some ⟨u, .ser, false⟩ } } u .running) :: out + | [] => out := out + return out.reverse + +def succ (c : Cfg) (s : St) : List (Act × St) := + mainSteps c s ++ workerSteps c s ++ + loaderSteps c s 1 s.l1 (fun t l => { t with l1 := l }) ++ + (if s.l2on then loaderSteps c s 2 s.l2 (fun t l => { t with l2 := l }) else []) + +def mainDone (c : Cfg) (s : St) : Bool := s.inl.isNone && (prog c)[s.pc]? == some .done + +def terminal (c : Cfg) (s : St) : Bool := + mainDone c s && s.workers.all (·.job.isNone) && s.l1.isEmpty && (s.l2.isEmpty || !s.l2on) + +/-! ### Properties -/ + +/-- P1: a rebuilt URI is binary-loadable (not in sources and a binary exists) only when complete. -/ +def p1 (s : St) : Bool := + (List.range 3).all fun u => s.task[u]! == .idle || s.inSrc[u]! || s.bin[u]! == Bin.none || s.bin[u]! == Bin.fresh + +/-- P2: when the build returns, every submitted store completed or was reported as not processed. -/ +def p2 (c : Cfg) (s : St) : Bool := + !mainDone c s || s.task.all fun t => t == .idle || t == .done || t == .failed || t == .dropped + +/-- P3: nobody reads a binary that is being written (partial) ... -/ +def p3partial (s : St) : Bool := !s.partialLd && !s.partialMain +/-- ... nor an outdated binary of a URI rebuilt in this build. -/ +def p3stale (s : St) : Bool := !s.staleLd && !s.staleMain +/-- P5: when everything has stopped, no rebuilt URI is left with an outdated binary on disk + (later builds load every non-source URI from its binary). -/ +def pEnd (c : Cfg) (s : St) : Bool := + !terminal c s || (List.range 3).all fun u => s.task[u]! == .idle || s.bin[u]! != .stale + +/-- P4: no unsynchronised concurrent access to the non-thread-safe sources HashSet. -/ +def p4 (s : St) : Bool := !s.setRace + +end BinaryStorage diff --git a/formal/binary-storage/lean/BinaryStorage/Proof.lean b/formal/binary-storage/lean/BinaryStorage/Proof.lean new file mode 100644 index 000000000..5052ef9ce --- /dev/null +++ b/formal/binary-storage/lean/BinaryStorage/Proof.lean @@ -0,0 +1,120 @@ +import BinaryStorage.Model + +/-! +All-sizes inductive-invariant proof of P1/P3 for the FIXED protocol. + +Abstraction: each URI carries its own store-lifecycle phase; the executor (any number of +workers, any queue capacity, CallerRunsPolicy, shutdown/shutdownNow, any number of clusters and +executor generations) only decides *which* URI steps next, so the global system is +"any URI takes one protocol step at a time", over an unbounded URI space (`Nat → U`). +The sources set is concurrent in the fix, so each set operation is one atomic step. +-/ +namespace BinaryStorage.Generic + +inductive GPh | idle | queued | ser | writing | written | done | dropped + deriving DecidableEq, Repr + +structure U where + rebuilt : Bool + inSrc : Bool + bin : Bin + ph : GPh + +/-- One step of the fixed per-URI protocol. -/ +inductive FStep : U → U → Prop + /-- installSourceLevelURIs / queueAffectedResources: URI becomes (re)built, added to sources. -/ + | mark (u : U) : FStep u { u with rebuilt := true, inSrc := true } + | submit (u : U) : u.rebuilt = true → u.ph = .idle → FStep u { u with ph := .queued } + | start (u : U) : u.ph = .queued → FStep u { u with ph := .ser } + /-- shutdownNow returns the task; fix deletes its outdated binary. -/ + | drop (u : U) : u.ph = .queued → FStep u { u with ph := .dropped, bin := .none } + | beginWrite (u : U) : u.ph = .ser → FStep u { u with ph := .writing, bin := .part } + /-- detached resource / IOException: fix deletes storage, keeps URI in sources. -/ + | failEarly (u : U) : u.ph = .ser → FStep u { u with ph := .done, bin := .none } + | endWrite (u : U) : u.ph = .writing → FStep u { u with ph := .written, bin := .fresh } + | abortWrite (u : U) : u.ph = .writing → FStep u { u with ph := .done, bin := .none } + /-- the only removal from sources: after the complete write. -/ + | remove (u : U) : u.ph = .written → FStep u { u with ph := .done, inSrc := false } + +/-- The code as written adds MCBS:656 — removal right after submission, in any phase. -/ +inductive BStep : U → U → Prop + | fixed (u v : U) : FStep u v → BStep u v + | mainRemove (u : U) : u.ph ≠ .idle → BStep u { u with inSrc := false } + +abbrev Sys := Nat → U + +def initial (σ : Sys) : Prop := ∀ k, (σ k).rebuilt = false ∧ (σ k).ph = .idle + +inductive Reach (R : U → U → Prop) : Sys → Prop + | init (σ : Sys) : initial σ → Reach R σ + | step (σ : Sys) (k : Nat) (v : U) : Reach R σ → R (σ k) v → + Reach R (fun j => if j = k then v else σ j) + +/-- Per-URI invariant. -/ +def Inv (u : U) : Prop := + (u.rebuilt = false → u.ph = .idle) ∧ + (u.rebuilt = true → (u.ph = .written → u.bin = .fresh) ∧ (u.inSrc = false → u.bin = .fresh ∧ u.ph = .done)) + +theorem inv_step {u v : U} (h : Inv u) (s : FStep u v) : Inv v := by + obtain ⟨h1, h2⟩ := h + cases s with + | mark => + refine ⟨by simp, fun _ => ⟨fun hw => ?_, by simp⟩⟩ + cases hr : u.rebuilt + · have := h1 hr; simp_all + · exact (h2 hr).1 hw + | submit hr hi => exact ⟨by simp_all, fun _ => ⟨by simp, fun hs => by have := (h2 hr).2 hs; simp_all⟩⟩ + | start hq => + refine ⟨fun hr => by have := h1 hr; simp_all, fun hr => ⟨by simp, fun hs => ?_⟩⟩ + have := (h2 hr).2 hs; simp_all + | drop hq => + refine ⟨fun hr => by have := h1 hr; simp_all, fun hr => ⟨by simp, fun hs => ?_⟩⟩ + have := (h2 hr).2 hs; simp_all + | beginWrite hq => + refine ⟨fun hr => by have := h1 hr; simp_all, fun hr => ⟨by simp, fun hs => ?_⟩⟩ + have := (h2 hr).2 hs; simp_all + | failEarly hq => + refine ⟨fun hr => by have := h1 hr; simp_all, fun hr => ⟨by simp, fun hs => ?_⟩⟩ + have := (h2 hr).2 hs; simp_all + | endWrite hq => + refine ⟨fun hr => by have := h1 hr; simp_all, fun hr => ⟨by simp, fun hs => ?_⟩⟩ + have := (h2 hr).2 hs; simp_all + | abortWrite hq => + refine ⟨fun hr => by have := h1 hr; simp_all, fun hr => ⟨by simp, fun hs => ?_⟩⟩ + have := (h2 hr).2 hs; simp_all + | remove hw => + refine ⟨fun hr => by have := h1 hr; simp_all, fun hr => ⟨by simp, fun _ => ?_⟩⟩ + exact ⟨(h2 hr).1 hw, rfl⟩ + +theorem inv_reach {σ : Sys} (h : Reach FStep σ) : ∀ k, Inv (σ k) := by + induction h with + | init σ hi => + intro k; obtain ⟨hr, hp⟩ := hi k + exact ⟨fun _ => hp, fun h => by simp_all⟩ + | step σ k v _ hs ih => + intro j + by_cases hj : j = k + · subst hj; simpa using inv_step (ih j) hs + · simpa [hj] using ih j + +/-- **P1 + P3 for all sizes (fixed protocol).** Whenever a rebuilt URI is binary-loadable + (not a source-level URI and a binary exists) the binary is completely written: no reader can + observe a partial or outdated binary, for any number of URIs, workers, clusters, interleavings. -/ +theorem fixed_safe {σ : Sys} (h : Reach FStep σ) (k : Nat) (hr : (σ k).rebuilt = true) + (hs : (σ k).inSrc = false) : (σ k).bin = .fresh := + ((inv_reach h k).2 hr).2 hs |>.1 + +/-- The same statement fails for the code as written (MCBS:656), already with one URI. -/ +theorem buggy_unsafe : ∃ σ, Reach BStep σ ∧ (σ 0).rebuilt = true ∧ (σ 0).inSrc = false ∧ (σ 0).bin = .stale := by + let σ0 : Sys := fun _ => { rebuilt := false, inSrc := false, bin := .stale, ph := .idle } + have r0 : Reach BStep σ0 := .init σ0 (fun _ => ⟨rfl, rfl⟩) + let u1 : U := { rebuilt := true, inSrc := true, bin := .stale, ph := .idle } + have r1 := Reach.step σ0 0 u1 r0 (.fixed _ _ (.mark _)) + let σ1 : Sys := fun j => if j = 0 then u1 else σ0 j + let u2 : U := { u1 with ph := .queued } + have r2 := Reach.step σ1 0 u2 r1 (.fixed _ _ (.submit _ (by simp [σ1, u1]) (by simp [σ1, u1]))) + let σ2 : Sys := fun j => if j = 0 then u2 else σ1 j + have r3 := Reach.step σ2 0 { u2 with inSrc := false } r2 (.mainRemove _ (by simp [σ2, u2])) + exact ⟨_, r3, by simp [u2, u1], by simp, by simp [u2, u1]⟩ + +end BinaryStorage.Generic diff --git a/formal/binary-storage/lean/BinaryStorage/Results.lean b/formal/binary-storage/lean/BinaryStorage/Results.lean new file mode 100644 index 000000000..08be7f4e1 --- /dev/null +++ b/formal/binary-storage/lean/BinaryStorage/Results.lean @@ -0,0 +1,52 @@ +import BinaryStorage.Check + +/-! +Machine-checked verdicts of the exhaustive BFS (bounded instance: 3 URIs, 2 clusters, +1-2 storage workers, queue capacity 0-1, 3 executor generations). `native_decide` trusts the +compiler; the BFS reaches a fixpoint (`complete`) so each verdict covers every interleaving. +-/ +namespace BinaryStorage + +/-! ### Fixed model: every property holds, every run terminates, no deadlock -/ +theorem fixed_default : allHold { fixed := true } = true := by native_decide +theorem fixed_two_workers_iofail : allHold { fixed := true, nW := 2, ioFail := true } = true := by native_decide +theorem fixed_caller_runs : allHold { fixed := true, qcap := 0, nW := 2, ioFail := true } = true := by native_decide +theorem fixed_no_old_binary : allHold { fixed := true, initBin := .none } = true := by native_decide + +/-! ### Sanity: planted bug (remove from sources before the write) is caught -/ +theorem planted_caught : ((report { fixed := true, plant := true }).p1).isSome = true := by native_decide + +/-! ### Code as written: violations -/ +/-- P4: unsynchronised concurrent access to the sources HashSet (7 steps). -/ +theorem bug_p4 : (report {}).p4 = some 7 := by native_decide +/-- P1: URI binary-loadable before its binary is written (MCBS:656), 7 steps. -/ +theorem bug_p1 : (report {}).p1 = some 7 := by native_decide +/-- P3 (stale), with atomic set semantics and without any timeout: next-cluster loader reads + the outdated binary of a URI rebuilt in the previous cluster (21 steps). -/ +theorem bug_stale_no_timeout : + (report { raceNondet := false, timeout := false }).p3stale = some 21 := by native_decide +/-- P3 (partial), atomic set semantics: loader reads a binary being written (22 steps). -/ +theorem bug_partial : (report { raceNondet := false }).p3partial = some 22 := by native_decide +/-- P2: store still running (neither completed nor reported) when the build returns (35 steps). -/ +theorem bug_p2 : (report {}).p2 = some 35 := by native_decide +/-- P5: an outdated binary survives the build: dropped store (timeout) ... -/ +theorem bug_pEnd_timeout : ((report { raceNondet := false }).pEnd).isSome = true := by native_decide +/-- ... or a swallowed IOException, even without timeouts and races. -/ +theorem bug_pEnd_iofail : + ((report { raceNondet := false, timeout := false, ioFail := true }).pEnd).isSome = true := by native_decide +/-- Without timeouts, IOException, dependency loading in loaders and HashSet races, only the + transient P1 window and the set race itself remain. -/ +theorem bug_minimal : + let r := report { raceNondet := false, timeout := false, touchDep := false } + r.p2.isNone && r.p3partial.isNone && r.p3stale.isNone && r.pEnd.isNone && r.p4.isSome = true := by + native_decide +/-- The bounded build always terminates and never deadlocks (code as written). -/ +theorem bug_terminates : let r := report {}; r.complete && r.acyclic && r.deadlocks == 0 = true := by + native_decide +/-- CallerRunsPolicy path is exercised, and a silent discard (execute on a shut-down pool) is unreachable. -/ +theorem caller_runs_reachable_discard_unreachable : + let g := explore { qcap := 0 } + (g.states.toList.any (·.inl.isSome)) && !(g.states.toList.any (·.task.contains .discarded)) = true := by + native_decide + +end BinaryStorage diff --git a/formal/binary-storage/lean/NOTES.md b/formal/binary-storage/lean/NOTES.md new file mode 100644 index 000000000..a911dee87 --- /dev/null +++ b/formal/binary-storage/lean/NOTES.md @@ -0,0 +1,252 @@ +# Binary-model storage: Lean model notes + +Subject: `MonitoredClusteringBuilderState` (MCBS), `com.avaloq.tools.ddk.xtext.builder`, its binary +storage executor, and the shared `SourceLevelURICache.sources` set, together with the DDK +`ParallelResourceLoader` (PRL) and Xtext 2.44 `ResourceStorageFacade` (RSF), `StorageAwareResource` +(SAR), `SourceLevelURIsAdapter`, and DDK `DirectLinkingResourceStorageFacade` (DLRSF). + +Build: `lake build` (toolchain `leanprover/lean4:v4.35.0-rc2`, no dependencies, no downloads). +A clean build takes about 8 s. Lean size: 617 lines (Model 338, Check 103, Proof 120, Results 52). +Wall time for the whole exercise: about 14 minutes. + +## Facts established from the code + +| Fact | Where | +|---|---| +| `sources` is a plain `HashSet` (not thread-safe) | Xtext `SourceLevelURICache:14` (`Sets.newHashSet()`) | +| The main resource set's adapter wraps that same set without a copy | MCBS:1536 → `SourceLevelURIsAdapter.setSourceLevelUrisWithoutCopy` | +| Every loader thread's local resource set gets the same view | PRL:168, PRL:174 | +| Every load asks `sources.contains(uri)`. If the URI is absent and a binary exists, it loads the binary | SAR:82-88 → RSF:49-54 (`doesStorageExist`); DLRSF:58-63 only adds the SKIP mode | +| Writers of `sources`: main thread `remove` right after submitting the store | MCBS:656 | +| Writers of `sources`: each storage worker `remove`s after `saveResource` (up to 4 at once) | MCBS:754 | +| Writers of `sources`: main thread `add` in `queueAffectedResources` | MCBS:1296 | +| The executor is fixed (4 threads, 15 000 queue slots) with `CallerRunsPolicy` | MCBS:181-192 | +| `awaitBinaryStorageExecutorTermination()` waits 1 minute with 0 retries. On timeout or interrupt it calls `shutdownNow()`, logs only a count, does not wait for running tasks, and replaces the executor | MCBS:803-872, MCBS:877-881 | +| The next cluster's loaders start before storage is awaited: `load(queue)` at L668-669 comes before `clearResourceSet` → await at L673/L1204 | MCBS:668-673, MCBS:1204 | +| `saveResource` swallows `IOException` from `writeResource` and leaves the old file in place. DLRSF deletes only on a thrown exception or when the resource has errors | RSF:95-104, DLRSF:70-80 | +| Nothing deletes the old binary of a URI that is being rebuilt. Only `toBeDeleted` URIs are cleaned | MCBS:452-453, MCBS:777-787 | + +## Model (`BinaryStorage/Model.lean`) + +The model covers one build with three URIs. Cluster 1 is `a` and `c`, both initial sources. +Cluster 2 is `b`: it is affected by `a`, becomes a source at L1296, and linking it resolves `a`. +Threads: +- the main builder thread, running the doUpdate program L529-690; +- a cluster-1 loader and a cluster-2 loader (PRL); +- the storage workers. Each executor generation has `nW` workers, and the model has 3 generations + because MCBS:871 recreates the pool. + +What the state tracks: +- per URI: `inSrc`, the binary state (`none | stale | part | fresh`), the store task state, + whether the resource is in the resource set, and whether it has been loaded; +- the executor: queue, `shut`, generation, and workers, including zombie workers left over from an + earlier generation; +- the CallerRuns inline job; +- in-flight HashSet operations; +- the hazard flags. + +Steps that are not atomic in the code are separate steps in the model: +- `contains`, `add` and `remove` each have a begin step and an end step; +- a store has four phases: serialize, write begins (binary becomes partial), write ends (binary + becomes fresh), and L754 removal (begin and end). + +The executor follows Java semantics: +- core worker threads are created lazily, then tasks queue until the capacity is reached; +- when the queue is full, CallerRuns runs the task on the main thread; after shutdown it silently + discards it; +- `shutdown` lets queued tasks drain; +- `awaitTermination` either returns true or times out (nondeterministically; this also stands for + an `InterruptedException`); +- `shutdownNow` drops the queued tasks and interrupts running ones, which keep running; +- an interrupted write fails, and DLRSF then deletes the storage. + +Configuration switches: + +| Switch | What it enables | +|---|---| +| `timeout` | `awaitTermination` may time out | +| `ioFail` | the IOException in `writeResource` is swallowed | +| `touchDep` | loading `b` in a loader thread also loads `a` into its local set | +| `raceNondet` | racing HashSet operations may miss a key or lose a write. With `false`, races are only flagged | +| `fixed` | applies the candidate fix | +| `plant` | adds a planted bug on top of the fix | + +Candidate fix (`fixed := true`), not applied to the Java: +1. Remove from `sources` only after the binary is completely written: drop L656 and keep L754. +2. Make `sources` a concurrent set. +3. Await storage termination before starting the next cluster's loaders. On timeout, wait for the + running tasks as well. +4. Delete the outdated binary of any store that did not complete (dropped, IOException, or + detached resource). + +Assumptions and abstractions: +- A loader is modelled as one sequential thread, where the code uses N threads. +- Linking and validation are atomic steps on the main thread. +- The watchdog and cancellation are left out. Findings F1-F3 of `formal/parallel-loader` are not + re-modelled: loaders always finish before the main thread consumes them. +- `touchDep` assumes a language whose load pulls in other resources. PRL:131-137 exists to handle + exactly that case. +- A racy `contains` may return a false "absent". This is backed by `HashMap.resize` publishing the + empty new table before the entries are transferred, and by removals from treeified bins. +- A racy write may be lost. + +## Properties + +| ID | Statement | +|---|---| +| P1 | A rebuilt URI that is not in sources and has a binary has a complete (`fresh`) binary | +| P2 | When the build returns, every submitted store is done, failed (and logged), or dropped (and reported) | +| P3 | No thread loads a partial binary (P3partial) or an outdated binary of a URI rebuilt in this build (P3stale) | +| P4 | No unsynchronised overlapping access to the `sources` HashSet | +| P5 (pEnd) | When everything has stopped, no rebuilt URI still has an outdated binary on disk | +| Termination | The reachable graph is acyclic (Kahn) and every non-terminal state has a successor | + +## Results + +All BFS runs reach a fixpoint. The Lean theorems are in `Results.lean` and `Proof.lean`. + +| Configuration | States | P1 | P2 | P3partial | P3stale | P4 | P5 | Acyclic, no deadlock | +|---|---|---|---|---|---|---|---|---| +| Code as written, defaults (1 worker, queue 1) | 15 699 | ✗7 | ✗35 | ✗22 | ✗8 | ✗7 | ✗38 | ✓ | +| Code, 2 workers | 70 908 | ✗ | ✗ | ✗ | ✗ | ✗ | ✗ | ✓ | +| Code, `ioFail` | 50 197 | ✗ | ✗ | ✗ | ✗ | ✗ | ✗ | ✓ | +| Code, queue 0 (CallerRuns reachable) | 7 097 | ✗ | ✗ | ✗ | ✗ | ✗ | ✓ | ✓ | +| Code, no timeout, no `touchDep`, no race nondeterminism | 508 | ✗ | ✓ | ✓ | ✓ | ✗ | ✓ | ✓ | +| Fixed (4 configurations, including 2 workers, CallerRuns, ioFail) | 105–240 | ✓ | ✓ | ✓ | ✓ | ✓ | ✓ | ✓ | +| Fixed plus planted bug (removal before the write) | 162 | ✗5 | | | | | | | + +In the table, ✗n means the property is violated and the shortest counterexample has n steps. + +What is proved and what is only bounded-checked: +- **Proved for all sizes, without `sorry`** (`Proof.lean`, `fixed_safe`): P1 and P3 for the fixed + protocol. + - This covers any number of URIs (`Nat → U`), workers, clusters, executor generations and + interleavings, with the executor abstracted to per-URI lifecycle phases. + - It uses only the `propext` axiom. + - `buggy_unsafe` proves that the same statement fails once the L656 removal is added. +- **Bounded, exhaustive, via `native_decide`**: P2, P4, P5, termination and deadlock freedom, and + every counterexample. + +Sanity checks: +- The fixed model passes P1-P5, termination and deadlock freedom in 4 configurations. +- The planted bug is caught by P1 in 5 steps. +- The CallerRuns path is reachable. +- The silent CallerRuns discard is unreachable (no `execute` on a pool that is shut down). + +## Findings + +Step numbers below refer to the traces printed by `cex`. Loader bookkeeping steps are elided. + +### B1: unsynchronised concurrent mutation of the `sources` HashSet (P4). CONFIRMED + +Shortest trace, 7 steps: +1. loader1: `contains(a)` (PRL:174 → RSF:51). +2. loader1 publishes `a`. +3. main `next()` and `addResource` (MCBS:537). +4. main `execute(store a)` (MCBS:726). +5. main `sources.remove(a)` begins (MCBS:656). +6. loader1 `contains(c)` begins (RSF:51) while the removal is still in flight. + +The same set is also written by up to 4 storage workers at once (MCBS:754), and by the main thread +at MCBS:1296 while workers from the previous cluster are still removing entries. There is no +synchronisation anywhere. + +Possible consequences, reproduced in the model with `raceNondet`: +- a spurious "absent" from `contains`, so a source URI is loaded from its old binary (P3stale in + 8 steps); +- a lost `add(b)` at L1296, so `b` is not a source when loader2 loads it, and the builder relinks + a resource loaded from its binary. `addResource` (MCBS:691-705) exists precisely to avoid that. + +These corruption outcomes are plausible under the Java Memory Model and HashMap internals but were +not demonstrated in Java. The data race itself is certain. + +### B2: URI becomes binary-loadable before its binary is written (P1). CONFIRMED + +MCBS:656 removes `changedURI` from `sources` on the main thread immediately after +`storeBinaryResource` only submitted the task. MCBS:754 does the same removal properly, after +`saveResource`. From this point until the write finishes, any load of the URI takes the binary +path (RSF:51-53). The P1 trace is the first 7 steps of B1. + +Taken alone this window is harmless: with no timeout, no dependency loading in loaders and no race +nondeterminism, P1 is violated but P2, P3 and P5 hold. B3-B6 are the paths that make it +observable. + +### B3: next cluster's loaders run before storage is awaited, and read partial or outdated binaries (P3). CONFIRMED (ordering); impact depends on the language + +MCBS:668-669 starts the loader for cluster N+1. The storage await happens only afterwards, inside +`clearResourceSet` (MCBS:673 → 1204). + +Stale-read trace, 21 steps, no timeout and atomic set semantics: +1. main `next(a)`; the store of `a` goes to a new worker (726); `remove(a)` (656). +2. main `next(c)`; the store of `c` is queued (726); `remove(c)` (656). +3. main `add(b)` (1296). +4. main starts loader2 (668-669). +5. loader2 `contains(b)` returns true, so it parses `b`. +6. Loading `b` pulls in `a`: `contains(a)` returns false (removed at 656). Worker0 has not started + writing yet, so loader2 loads `a`'s **binary from the previous build** (SAR:86). + +Partial-read trace, 22 steps: the same interleaving, with worker0 already at `generateFile` +(RSF:104) when loader2 reads. + +Impact: +- A truncated binary usually throws `IOException`, and SAR:89-90 then falls back to parsing, which + mitigates the partial read. +- An outdated but complete binary is accepted silently. +- This needs a language whose load pulls in referenced resources (`touchDep`). With + `touchDep := false` the loader only ever asks about its own URI, which is still a source. + +### B4: after an await timeout, stores are silently lost and the main thread links against outdated binaries (P3stale, P5). CONFIRMED + +The default await is 1 minute with 0 retries (MCBS:804). A backlog of more than a minute makes it +fail: for example, 15 000 queue slots with 4 workers only needs about 16 ms per store. +`shutdownNow` (MCBS:879) then drops the queued stores and logs only their count. + +Their URIs were already removed from `sources` at L656, so they stay binary-loadable with the old +file on disk. Trace (P3stale on the main thread), 29 steps: +- steps 1-17 as in B3; +- 18: `shutdown` (826); +- 19: `awaitTermination` times out, then `shutdownNow` (837, 879); the store of `c` is dropped; +- 20: the executor is recreated (871); +- 21: `clearResourceSet` (1207); +- 27-29: main `next(b)`, then `resolveLazyCrossReferences` loads `a`: `contains(a)` returns false, + and the **outdated binary** of `a` is loaded (MCBS:564, SAR:86). + +P5 trace, 38 steps: the dropped store of `c` leaves `c`'s old binary on disk. Later builds install +only `toBeUpdated` and queue URIs as sources (MCBS:1524-1536), so every later build loads the +outdated binary until `c` changes again. The problem persists beyond the build. + +### B5: running stores are neither completed nor reported when the build returns (P2). CONFIRMED + +`terminateBinaryStorageExecutor` never waits after `shutdownNow`. Running tasks keep going as +zombies: they write binaries and mutate `sources`, and nothing awaits them. Meanwhile: +- the main thread clears the resource set they are serializing (MCBS:1207; the comment at MCBS:1203 + names exactly this hazard); +- the main thread starts the next cluster; +- `doUpdate` returns. + +Trace, 35 steps: B4 up to step 29; the store of `b` goes to a gen-1 worker (726); `remove(b)` +(656); the finally block's await times out and calls `shutdownNow` (684 → 879); `doUpdate` returns +while `b`'s store is still running. Only queued tasks are counted in "{} tasks not processed" +(MCBS:880). The running ones are not. + +### B6: an IOException swallowed by Xtext leaves an outdated binary that is treated as valid (P5). CONFIRMED (code path); trigger is rare + +- RSF:97-103 catches the `IOException` from `writeResource`, logs a warning and returns normally + without touching the old file. +- DLRSF:70-80 deletes storage only when an exception is thrown. +- MCBS:754 then removes the URI from `sources`. + +Trace, 45 steps, no timeout and no race: the IOException hits at step 8 for `a` and at step 23 for +`c`. At step 32 loader2 loads `a`'s outdated binary, at step 36 main does the same, and the files +stay outdated after the build. + +### Not findings + +- **Termination and deadlock freedom:** hold in every configuration (bounded). There are no cycles + and no stuck states. +- **CallerRunsPolicy:** reachable. A silent discard would need `execute` after `shutdown`, which + never happens: only the main thread submits stores, and it always recreates the executor right + after shutting it down. +- **Serialization of a detached resource after a timeout:** modelled as the store failing and + DLRSF deleting the storage, which is safe. This is a MODEL-SIMPLIFICATION: whether serialization + of a detached resource succeeds or throws was not checked in the DDK writable. diff --git a/formal/binary-storage/lean/lake-manifest.json b/formal/binary-storage/lean/lake-manifest.json new file mode 100644 index 000000000..2b78d9f48 --- /dev/null +++ b/formal/binary-storage/lean/lake-manifest.json @@ -0,0 +1,6 @@ +{"version": "1.2.0", + "packagesDir": ".lake/packages", + "packages": [], + "name": "BinaryStorage", + "lakeDir": ".lake", + "fixedToolchain": false} diff --git a/formal/binary-storage/lean/lakefile.toml b/formal/binary-storage/lean/lakefile.toml new file mode 100644 index 000000000..6531b0138 --- /dev/null +++ b/formal/binary-storage/lean/lakefile.toml @@ -0,0 +1,6 @@ +name = "BinaryStorage" +version = "0.1.0" +defaultTargets = ["BinaryStorage"] + +[[lean_lib]] +name = "BinaryStorage" diff --git a/formal/binary-storage/lean/lean-toolchain b/formal/binary-storage/lean/lean-toolchain new file mode 100644 index 000000000..acc704ffe --- /dev/null +++ b/formal/binary-storage/lean/lean-toolchain @@ -0,0 +1 @@ +leanprover/lean4:v4.35.0-rc2 diff --git a/formal/binary-storage/lean/theorems.txt b/formal/binary-storage/lean/theorems.txt new file mode 100644 index 000000000..381eda240 --- /dev/null +++ b/formal/binary-storage/lean/theorems.txt @@ -0,0 +1,20 @@ +# ; checked by formal/check.sh via #print axioms +BinaryStorage.bug_minimal native_decide +BinaryStorage.bug_p1 native_decide +BinaryStorage.bug_p2 native_decide +BinaryStorage.bug_p4 native_decide +BinaryStorage.bug_partial native_decide +BinaryStorage.bug_pEnd_iofail native_decide +BinaryStorage.bug_pEnd_timeout native_decide +BinaryStorage.bug_stale_no_timeout native_decide +BinaryStorage.bug_terminates native_decide +BinaryStorage.caller_runs_reachable_discard_unreachable native_decide +BinaryStorage.fixed_caller_runs native_decide +BinaryStorage.fixed_default native_decide +BinaryStorage.fixed_no_old_binary native_decide +BinaryStorage.fixed_two_workers_iofail native_decide +BinaryStorage.Generic.buggy_unsafe kernel +BinaryStorage.Generic.fixed_safe kernel +BinaryStorage.Generic.inv_reach kernel +BinaryStorage.Generic.inv_step kernel +BinaryStorage.planted_caught native_decide diff --git a/formal/binary-storage/tla/BinaryStorage.tla b/formal/binary-storage/tla/BinaryStorage.tla new file mode 100644 index 000000000..1aad7faa0 --- /dev/null +++ b/formal/binary-storage/tla/BinaryStorage.tla @@ -0,0 +1,488 @@ +---------------------------- MODULE BinaryStorage ---------------------------- +(***************************************************************************) +(* Binary-model storage in MonitoredClusteringBuilderState (MCBS) and its *) +(* interaction with the cluster loop, the shared source-level URI set and *) +(* the ParallelResourceLoader (PRL) threads of the current/next cluster. *) +(* *) +(* MCBS = com.avaloq.tools.ddk.xtext.builder/src/com/avaloq/tools/ddk/ *) +(* xtext/builder/MonitoredClusteringBuilderState.java *) +(* PRL = .../xtext/builder/resourceloader/ParallelResourceLoader.java *) +(* *) +(* Actors: builder (main) thread; binary-storage ThreadPoolExecutor *) +(* workers, one executor per "generation" (MCBS:871 creates a new one *) +(* after every await); PRL loader jobs (one per queued URI). *) +(* *) +(* All Fix*/Plant* flags FALSE = the code as written. *) +(***************************************************************************) +EXTENDS Integers, Sequences, FiniteSets + +CONSTANTS + Clusters, \* sequence of URI sets: Clusters[1] = toBeUpdated, Clusters[k+1] = affected by cluster k + Deps, \* [URIs -> SUBSET URIs]: resources whose load may be triggered when linking/loading u + NStore, \* BINARY_STORAGE_EXECUTOR_PARALLELISM (MCBS:124) + QCap, \* BINARY_STORAGE_EXECUTOR_QUEUE_CAPACITY (MCBS:125), >= 1 + MaxTimeouts, \* bound on awaitTermination timeouts / interrupts of the builder (MCBS:837, 865) + LoaderLoadsDeps, \* may a PRL job's load of u also load u's dependencies in its local resource set? + AllowLoadFail, \* may a PRL job return an exception (LoadOperationException(uri), MCBS:595-597)? + AllowLinkFail, \* may linking throw an Exception after addResource (outer catch, MCBS:585-613)? + FixA, \* drop the main-thread sources.remove (MCBS:656); rely on MCBS:754 + FixB, \* sources set is thread-safe (every access atomic) + FixC, \* after shutdownNow, keep waiting until running store tasks have finished + FixD, \* do not store a resource whose processing threw (MCBS:654 skipped) + PlantBug \* planted: worker removes from sources BEFORE writing the binary + +URIs == UNION {Clusters[i] : i \in 1..Len(Clusters)} +NC == Len(Clusters) +Gens == 1..(NC + 1) \* one executor per await (NC-1 between clusters + 1 final) + the fresh one +WIds == Gens \X (1..NStore) +NoURI == "-" \* placeholder for URI-typed variables +NoTask == <<"-", 0>> \* placeholder for store-task variables (task = <>) +LDeps(u) == IF LoaderLoadsDeps THEN {u} \cup Deps[u] ELSE {u} \* shouldLoadFromStorage(u) is always asked for u itself + +ASSUME /\ NC >= 1 /\ NStore >= 1 /\ QCap >= 1 /\ MaxTimeouts \in Nat + /\ \A u \in URIs : Deps[u] \subseteq URIs + +VARIABLES + \* builder thread + mpc, k, queue, cur, depsTodo, mdep, mainRS, live, toAdd, qcur, gen, aret, timeouts, macc, + \* shared state + sources, \* SourceLevelURICache.getSources(): a plain java.util.HashSet (Xtext SourceLevelURICache.) + inBuild, \* URIs that are (re)built in this build (entered sources via install/queueAffected) + binary, \* on-disk binary per URI: "old" (previous build) | "none" | "partial" | "new" + \* PRL loader jobs + lpc, ltodo, lcur, lres, lacc, + \* storage executors and workers + est, eq, nstarted, wpc, wtask, wintr, wacc, + \* history + sst, \* per URI store status: no | queued | running | ok | failed | dropped | discarded + reads, \* set of <>: binary actually opened + detached \* a store serialised a resource no longer in the builder's resource set + +mainVars == <> +loadVars == <> +execVars == <> +workVars == <> +vars == <> + +Init == + /\ mpc = "head" /\ k = 1 /\ queue = Clusters[1] /\ cur = NoURI + /\ depsTodo = {} /\ mdep = NoURI /\ mainRS = {} /\ live = {} + /\ toAdd = {} /\ qcur = NoURI /\ gen = 1 /\ aret = "none" /\ timeouts = 0 /\ macc = "none" + /\ sources = Clusters[1] \* installSourceLevelURIs (MCBS:454, 1524-1536) + /\ inBuild = Clusters[1] + /\ binary \in [URIs -> {"old", "none"}] + /\ lpc = [u \in URIs |-> IF u \in Clusters[1] THEN "run" ELSE "off"] \* loadOperation.load(queue) MCBS:510 + /\ ltodo = [u \in URIs |-> IF u \in Clusters[1] THEN LDeps(u) ELSE {}] + /\ lcur = [u \in URIs |-> NoURI] /\ lres = [u \in URIs |-> "none"] /\ lacc = [u \in URIs |-> "none"] + /\ est = [g \in Gens |-> "running"] /\ eq = [g \in Gens |-> <<>>] /\ nstarted = [g \in Gens |-> 0] + /\ wpc = [w \in WIds |-> "none"] /\ wtask = [w \in WIds |-> NoTask] + /\ wintr = [w \in WIds |-> FALSE] /\ wacc = [w \in WIds |-> "none"] + /\ sst = [u \in URIs |-> "no"] /\ reads = {} /\ detached = FALSE + +----------------------------------------------------------------------------- +(* Builder thread *) + +\* Inner loop head: next() returns a finished PRL job (MCBS:531-556). +MHead == + /\ mpc = "head" + /\ IF queue = {} + THEN /\ mpc' = "endCluster" + /\ UNCHANGED <> + ELSE \E u \in queue : + /\ lpc[u] = "deliv" + /\ lpc' = [lpc EXCEPT ![u] = "done"] + /\ cur' = u + /\ queue' = queue \ {u} \* MCBS:556 / MCBS:604 + /\ IF lres[u] = "fail" + THEN \* LoadOperationException(uri): resource stays null, no store (MCBS:595-613, 654) + /\ mpc' = "rmsrc1" + /\ UNCHANGED <> + ELSE /\ mainRS' = mainRS \cup {u} \* addResource MCBS:553 + /\ live' = live \cup {<>} + /\ depsTodo' = Deps[u] + /\ mpc' = "link" + /\ UNCHANGED <> + +\* resolveLazyCrossReferences (MCBS:569): loads dependencies into the builder's resource set. +Link == + /\ mpc = "link" + /\ IF depsTodo = {} + THEN \/ /\ mpc' = "submit" /\ UNCHANGED <> + \/ /\ AllowLinkFail \* exception after addResource: + /\ live' = live \ {<>} \* resourceSet.getResources().remove(resource) MCBS:608 + /\ mainRS' = mainRS \ {cur} + /\ mpc' = IF FixD THEN "rmsrc1" ELSE "submit" \* MCBS:654 still stores it + /\ UNCHANGED <> + ELSE \E d \in depsTodo : + IF d \in mainRS + THEN /\ depsTodo' = depsTodo \ {d} + /\ UNCHANGED <> + ELSE /\ mdep' = d + /\ macc' = IF FixB THEN "none" ELSE "r" \* shouldLoadFromStorage: sources.contains(d) + /\ mpc' = "linkChk" + /\ UNCHANGED <> + /\ UNCHANGED <> + +LinkChk == + /\ mpc = "linkChk" + /\ macc' = "none" + /\ reads' = IF mdep \notin sources /\ binary[mdep] # "none" + THEN reads \cup {<<"main", mdep, binary[mdep], mdep \in inBuild>>} + ELSE reads + /\ mainRS' = mainRS \cup {mdep} + /\ depsTodo' = depsTodo \ {mdep} + /\ mpc' = "link" + /\ UNCHANGED <> + +\* storeBinaryResource (MCBS:716-736) -> ThreadPoolExecutor.execute with CallerRunsPolicy. +Submit == + /\ mpc = "submit" + /\ LET g == gen + t == <> + w == <> + IN IF est[g] # "running" + THEN \* CallerRunsPolicy.rejectedExecution: silently discards when shut down + /\ sst' = [sst EXCEPT ![cur] = "discarded"] + /\ mpc' = "rmsrc1" + /\ UNCHANGED <> + ELSE IF nstarted[g] < NStore + THEN \* workerCount < corePoolSize: addWorker(command, true) + /\ nstarted' = [nstarted EXCEPT ![g] = @ + 1] + /\ wpc' = [wpc EXCEPT ![w] = "ser"] + /\ wtask' = [wtask EXCEPT ![w] = t] + /\ sst' = [sst EXCEPT ![cur] = "running"] + /\ mpc' = "rmsrc1" + /\ UNCHANGED eq + ELSE IF Len(eq[g]) < QCap + THEN /\ eq' = [eq EXCEPT ![g] = Append(@, t)] + /\ sst' = [sst EXCEPT ![cur] = "queued"] + /\ mpc' = "rmsrc1" + /\ UNCHANGED <> + ELSE \* queue full: CallerRunsPolicy runs doStoreBinaryResource on the builder thread + /\ sst' = [sst EXCEPT ![cur] = "running"] + /\ mpc' = "crSer" + /\ UNCHANGED <> + /\ UNCHANGED <> + +\* doStoreBinaryResource on the builder thread (CallerRunsPolicy). +CrSer == + /\ mpc = "crSer" + /\ detached' = (detached \/ <> \notin live) + /\ mpc' = "crWrite" + /\ UNCHANGED <> + +CrWrite == + /\ mpc = "crWrite" + /\ \/ /\ binary' = [binary EXCEPT ![cur] = "partial"] /\ mpc' = "crWriteEnd" \* fsa.generateFile starts + \/ /\ binary' = [binary EXCEPT ![cur] = "none"] /\ mpc' = "crRm1" \* errors: deleteStorage + /\ UNCHANGED <> + +CrWriteEnd == + /\ mpc = "crWriteEnd" + /\ binary' = [binary EXCEPT ![cur] = "new"] + /\ mpc' = "crRm1" + /\ UNCHANGED <> + +CrRm1 == \* MCBS:754 + /\ mpc = "crRm1" + /\ IF FixB + THEN /\ sources' = sources \ {cur} /\ sst' = [sst EXCEPT ![cur] = "ok"] /\ mpc' = "rmsrc1" + /\ UNCHANGED macc + ELSE /\ macc' = "w" /\ mpc' = "crRm2" /\ UNCHANGED <> + /\ UNCHANGED <> + +CrRm2 == + /\ mpc = "crRm2" + /\ sources' = sources \ {cur} /\ macc' = "none" + /\ sst' = [sst EXCEPT ![cur] = "ok"] + /\ mpc' = "rmsrc1" + /\ UNCHANGED <> + +\* buildData.getSourceLevelURICache().getSources().remove(changedURI) (MCBS:656) +RmSrc1 == + /\ mpc = "rmsrc1" + /\ IF FixA + THEN /\ mpc' = "head" /\ UNCHANGED <> + ELSE IF FixB + THEN /\ sources' = sources \ {cur} /\ mpc' = "head" /\ UNCHANGED macc + ELSE /\ macc' = "w" /\ mpc' = "rmsrc2" /\ UNCHANGED sources + /\ UNCHANGED <> + +RmSrc2 == + /\ mpc = "rmsrc2" + /\ sources' = sources \ {cur} /\ macc' = "none" + /\ mpc' = "head" + /\ UNCHANGED <> + +\* Inner loop exit: loadOperation.cancel() (MCBS:661), then queueAffectedResources (MCBS:663). +EndCluster == + /\ mpc = "endCluster" + /\ IF k < NC + THEN /\ toAdd' = Clusters[k + 1] /\ mpc' = "qa" + ELSE /\ mpc' = "exitLoop" /\ UNCHANGED toAdd + /\ UNCHANGED <> + +\* queueAffectedResources: buildData.queueURI(uri); sources.add(uri) (MCBS:1296-1298, 1312-1314) +QA == + /\ mpc = "qa" + /\ IF toAdd = {} + THEN /\ mpc' = "newLoad" /\ UNCHANGED <> + ELSE \E u \in toAdd : + /\ queue' = queue \cup {u} + /\ IF FixB + THEN /\ sources' = sources \cup {u} /\ inBuild' = inBuild \cup {u} + /\ toAdd' = toAdd \ {u} /\ mpc' = "qa" /\ UNCHANGED <> + ELSE /\ qcur' = u /\ macc' = "w" /\ mpc' = "qa2" + /\ UNCHANGED <> + /\ UNCHANGED <> + +QA2 == + /\ mpc = "qa2" + /\ sources' = sources \cup {qcur} /\ inBuild' = inBuild \cup {qcur} + /\ toAdd' = toAdd \ {qcur} /\ macc' = "none" /\ mpc' = "qa" + /\ UNCHANGED <> + +\* if (!queue.isEmpty()) { loadOperation = create(...); loadOperation.load(queue); } (MCBS:667-670) +\* -- the next cluster's PRL jobs start BEFORE clearResourceSet awaits the storage executor (MCBS:672-674). +NewLoad == + /\ mpc = "newLoad" + /\ IF queue # {} + THEN /\ lpc' = [u \in URIs |-> IF u \in queue THEN "run" ELSE lpc[u]] + /\ ltodo' = [u \in URIs |-> IF u \in queue THEN LDeps(u) ELSE ltodo[u]] + /\ mpc' = "clear" + ELSE /\ mpc' = "exitLoop" /\ UNCHANGED <> + /\ UNCHANGED <> + +Terminated(g) == + /\ est[g] # "running" /\ eq[g] = <<>> + /\ \A i \in 1..NStore : wpc[<>] \in {"none", "exit"} + +\* awaitBinaryStorageExecutorTermination: from clearResourceSet (MCBS:1204) or finally (MCBS:684). +AwShut == + /\ mpc \in {"clear", "exitLoop"} + /\ est' = [est EXCEPT ![gen] = IF @ = "running" THEN "shutdown" ELSE @] \* shutdown() MCBS:826 + /\ aret' = mpc + /\ mpc' = "awWait" + /\ UNCHANGED <> + +AwOk == \* awaitTermination returns true (MCBS:837, 859) + /\ mpc = "awWait" + /\ Terminated(gen) + /\ mpc' = "awDone" + /\ UNCHANGED <> + +\* awaitTermination times out (retryCount = 0 -> loop exits) or throws InterruptedException: +\* terminateBinaryStorageExecutor -> shutdownNow() (MCBS:838-867, 877-881). +AwTimeout == + /\ mpc = "awWait" + /\ ~Terminated(gen) + /\ timeouts < MaxTimeouts + /\ timeouts' = timeouts + 1 + /\ est' = [est EXCEPT ![gen] = "stop"] + /\ sst' = [u \in URIs |-> IF \E i \in 1..Len(eq[gen]) : eq[gen][i][1] = u THEN "dropped" ELSE sst[u]] + /\ eq' = [eq EXCEPT ![gen] = <<>>] \* "{} tasks not processed" + /\ wintr' = [w \in WIds |-> IF w[1] = gen /\ wpc[w] \notin {"none", "exit"} THEN TRUE ELSE wintr[w]] + /\ mpc' = IF FixC THEN "awDrain" ELSE "awDone" + /\ UNCHANGED <> + +AwDrain == \* FixC only: wait for running tasks after shutdownNow + /\ mpc = "awDrain" + /\ Terminated(gen) + /\ mpc' = "awDone" + /\ UNCHANGED <> + +\* binaryStorageExecutor = makeBinaryStorageExecutor() (MCBS:871); then clear the resource set (MCBS:1207) +AwDone == + /\ mpc = "awDone" + /\ gen' = gen + 1 + /\ IF aret = "clear" + THEN /\ mainRS' = {} /\ live' = {} /\ k' = k + 1 /\ mpc' = "head" + ELSE /\ mpc' = "done" /\ UNCHANGED <> + /\ UNCHANGED <> + +MainStep == MHead \/ Link \/ LinkChk \/ Submit \/ CrSer \/ CrWrite \/ CrWriteEnd \/ CrRm1 \/ CrRm2 + \/ RmSrc1 \/ RmSrc2 \/ EndCluster \/ QA \/ QA2 \/ NewLoad \/ AwShut \/ AwOk \/ AwDrain \/ AwDone + +----------------------------------------------------------------------------- +(* Storage workers: doStoreBinaryResource (MCBS:746-769) *) + +WTake(w) == + LET g == w[1] IN + /\ wpc[w] = "idle" + /\ IF est[g] = "stop" \/ (est[g] = "shutdown" /\ eq[g] = <<>>) + THEN /\ wpc' = [wpc EXCEPT ![w] = "exit"] /\ UNCHANGED <> + ELSE /\ eq[g] # <<>> + /\ wtask' = [wtask EXCEPT ![w] = Head(eq[g])] + /\ eq' = [eq EXCEPT ![g] = Tail(@)] + /\ sst' = [sst EXCEPT ![Head(eq[g])[1]] = "running"] + /\ wpc' = [wpc EXCEPT ![w] = "ser"] + /\ UNCHANGED <> + +\* createResourceStorageWritable(bout).writeResource(resource): serialises the EMF resource in memory +WSer(w) == + /\ wpc[w] = "ser" + /\ detached' = (detached \/ wtask[w] \notin live) + /\ wpc' = [wpc EXCEPT ![w] = IF PlantBug THEN "rm1" ELSE "write"] + /\ UNCHANGED <> + +WWrite(w) == + LET u == wtask[w][1] IN + /\ wpc[w] = "write" + /\ \/ /\ binary' = [binary EXCEPT ![u] = "partial"] \* fsa.generateFile in progress + /\ wpc' = [wpc EXCEPT ![w] = "wend"] /\ UNCHANGED sst + \/ /\ binary' = [binary EXCEPT ![u] = "none"] \* resource has errors: deleteStorage (DLRSF:72-76) + /\ wpc' = [wpc EXCEPT ![w] = "rm1"] /\ UNCHANGED sst + /\ UNCHANGED <> + +WWriteEnd(w) == + LET u == wtask[w][1] IN + /\ wpc[w] = "wend" + /\ \/ /\ binary' = [binary EXCEPT ![u] = "new"] + /\ wpc' = [wpc EXCEPT ![w] = IF PlantBug THEN "fin" ELSE "rm1"] /\ UNCHANGED sst + \/ /\ wintr[w] \* interrupted write throws: catch deletes storage, + /\ binary' = [binary EXCEPT ![u] = "none"] \* rethrow, logged (DLRSF:77-79, MCBS:765-767) + /\ sst' = [sst EXCEPT ![u] = "failed"] + /\ wpc' = [wpc EXCEPT ![w] = "idle"] + /\ UNCHANGED <> + +WRm1(w) == \* getSources().remove(resource.getURI()) (MCBS:754) + LET u == wtask[w][1] IN + /\ wpc[w] = "rm1" + /\ IF FixB + THEN /\ sources' = sources \ {u} + /\ wpc' = [wpc EXCEPT ![w] = IF PlantBug THEN "write" ELSE "fin"] + /\ UNCHANGED wacc + ELSE /\ wacc' = [wacc EXCEPT ![w] = "w"] /\ wpc' = [wpc EXCEPT ![w] = "rm2"] /\ UNCHANGED sources + /\ UNCHANGED <> + +WRm2(w) == + LET u == wtask[w][1] IN + /\ wpc[w] = "rm2" + /\ sources' = sources \ {u} /\ wacc' = [wacc EXCEPT ![w] = "none"] + /\ wpc' = [wpc EXCEPT ![w] = IF PlantBug THEN "write" ELSE "fin"] + /\ UNCHANGED <> + +WFin(w) == + /\ wpc[w] = "fin" + /\ sst' = [sst EXCEPT ![wtask[w][1]] = "ok"] + /\ wpc' = [wpc EXCEPT ![w] = "idle"] + /\ UNCHANGED <> + +WStep(w) == WTake(w) \/ WSer(w) \/ WWrite(w) \/ WWriteEnd(w) \/ WRm1(w) \/ WRm2(w) \/ WFin(w) + +----------------------------------------------------------------------------- +(* PRL jobs: localResourceSet.getResource(uri, true) (PRL:344-349) *) +(* StorageAwareResource.load -> shouldLoadFromStorage: sources.contains(d) *) +(* via the SourceLevelURIsAdapter installed WITHOUT copy (PRL:168-174). *) + +LRun(u) == + /\ lpc[u] = "run" + /\ IF ltodo[u] = {} + THEN /\ lres' = [lres EXCEPT ![u] = "ok"] \/ (AllowLoadFail /\ lres' = [lres EXCEPT ![u] = "fail"]) + /\ lpc' = [lpc EXCEPT ![u] = "deliv"] + /\ UNCHANGED <> + ELSE \E d \in ltodo[u] : + /\ lcur' = [lcur EXCEPT ![u] = d] + /\ lacc' = [lacc EXCEPT ![u] = IF FixB THEN "none" ELSE "r"] + /\ lpc' = [lpc EXCEPT ![u] = "chk"] + /\ UNCHANGED <> + /\ UNCHANGED <> + +LChk(u) == + LET d == lcur[u] IN + /\ lpc[u] = "chk" + /\ lacc' = [lacc EXCEPT ![u] = "none"] + /\ reads' = IF d \notin sources /\ binary[d] # "none" + THEN reads \cup {<<"loader", d, binary[d], d \in inBuild>>} + ELSE reads + /\ ltodo' = [ltodo EXCEPT ![u] = @ \ {d}] + /\ lpc' = [lpc EXCEPT ![u] = "run"] + /\ UNCHANGED <> + +LStep(u) == LRun(u) \/ LChk(u) + +----------------------------------------------------------------------------- +Next == MainStep \/ AwTimeout \/ (\E w \in WIds : WStep(w)) \/ (\E u \in URIs : LStep(u)) + +Spec == Init /\ [][Next]_vars + /\ WF_vars(MainStep) + /\ \A w \in WIds : WF_vars(WStep(w)) + /\ \A u \in URIs : WF_vars(LStep(u)) + +----------------------------------------------------------------------------- +(* Properties *) + +TypeOK == + /\ sources \subseteq URIs /\ inBuild \subseteq URIs + /\ binary \in [URIs -> {"old", "none", "partial", "new"}] + /\ sst \in [URIs -> {"no", "queued", "running", "ok", "failed", "dropped", "discarded"}] + /\ gen \in Gens /\ k \in 1..NC + +\* P1: a URI rebuilt in this build is "not in sources" (= binary-loadable) only once its store has run +\* to completion (binary "new", or deleted because of errors/failure) -- not queued, not dropped, not +\* skipped, not in the middle of serialising/writing. +Writing(u) == + \/ sst[u] = "queued" + \/ \E w \in WIds : wtask[w][1] = u /\ wpc[w] \in {"ser", "write", "wend"} + \/ cur = u /\ mpc \in {"crSer", "crWrite", "crWriteEnd"} +NotSourceOnlyWhenStored == + \A u \in inBuild : u \notin sources => (sst[u] \in {"running", "ok", "failed"} /\ ~Writing(u)) + +\* P2a: at the end of the build no store is silently lost or still queued. +StoresAccounted == + mpc = "done" => \A u \in URIs : sst[u] \notin {"queued", "discarded"} +\* P2b: every submitted store eventually completes or is reported as not processed. +StoreResolved == + \A u \in URIs : (sst[u] \in {"queued", "running"}) ~> (sst[u] \in {"ok", "failed", "dropped"}) + +\* P3: PRL jobs never open a binary that is still being written. +LoaderNoPartialRead == \A r \in reads : r[1] = "loader" => r[3] # "partial" +\* P3': same for the builder thread (linking). +MainNoPartialRead == \A r \in reads : r[1] = "main" => r[3] # "partial" +\* P3'': nobody opens the previous build's binary of a resource that is rebuilt in this build. +NoStaleRead == \A r \in reads : ~(r[3] = "old" /\ r[4]) + +\* P4: the (non-thread-safe) HashSet is never mutated concurrently with any other access. +NWriters == (IF macc = "w" THEN 1 ELSE 0) + Cardinality({u \in URIs : lacc[u] = "w"}) + Cardinality({w \in WIds : wacc[w] = "w"}) +NAccesses == (IF macc # "none" THEN 1 ELSE 0) + Cardinality({u \in URIs : lacc[u] # "none"}) + Cardinality({w \in WIds : wacc[w] # "none"}) +SetThreadSafe == NWriters > 0 => NAccesses = 1 + +\* P4 refinements, to classify which overlaps exist. +NoReadDuringWrite == NWriters > 0 => \A u \in URIs : lacc[u] = "none" \* loader contains() vs a mutation +NoAddDuringRemove == ~(mpc = "qa2" /\ \E w \in WIds : wacc[w] = "w") \* main add (MCBS:1298) vs worker remove (MCBS:754) + +\* P6: never serialise a resource that was removed from / cleared out of the builder's resource set. +NoDetachedStore == ~detached + +\* P5: termination. +BuildTerminates == <>(mpc = "done") +WorkersQuiesce == <>[](\A w \in WIds : wpc[w] \in {"none", "exit", "idle"}) + +\* Witnesses (should be VIOLATED: they show that the good/interesting paths are reachable). +WitnessDone == mpc # "done" +WitnessSecondClust == k < 2 +WitnessCallerRuns == mpc # "crSer" +WitnessTimeout == timeouts = 0 +WitnessGoodRead == \A r \in reads : r[3] # "new" +WitnessStoreOk == \A u \in URIs : sst[u] # "ok" +============================================================================= diff --git a/formal/binary-storage/tla/MC.tla b/formal/binary-storage/tla/MC.tla new file mode 100644 index 000000000..7b369ee46 --- /dev/null +++ b/formal/binary-storage/tla/MC.tla @@ -0,0 +1,16 @@ +------------------------------- MODULE MC ------------------------------- +(* Instantiation sizes for BinaryStorage (cfg files cannot write sequences/functions). *) +EXTENDS BinaryStorage +\* S: one resource per cluster; b depends on a. +ClustersS == << {"a"}, {"b"} >> +DepsS == [u \in {"a", "b"} |-> IF u = "b" THEN {"a"} ELSE {}] +\* M: two resources in cluster 1 (a2 depends on a1), b depends on both. +ClustersM == << {"a1", "a2"}, {"b"} >> +DepsM == [u \in {"a1", "a2", "b"} |-> CASE u = "a2" -> {"a1"} [] u = "b" -> {"a1", "a2"} [] OTHER -> {}] +\* L: three clusters. +ClustersL == << {"a1", "a2"}, {"b"}, {"c"} >> +DepsL == [u \in {"a1", "a2", "b", "c"} |-> CASE u = "a2" -> {"a1"} [] u = "b" -> {"a1"} [] u = "c" -> {"b"} [] OTHER -> {}] +\* R: three resources in cluster 1 so that NStore=1, QCap=1 fills the executor (CallerRunsPolicy). +ClustersR == << {"a1", "a2", "a3"}, {"b"} >> +DepsR == [u \in {"a1", "a2", "a3", "b"} |-> CASE u = "b" -> {"a1"} [] OTHER -> {}] +============================================================================= diff --git a/formal/binary-storage/tla/NOTES.md b/formal/binary-storage/tla/NOTES.md new file mode 100644 index 000000000..0ff1c5c3e --- /dev/null +++ b/formal/binary-storage/tla/NOTES.md @@ -0,0 +1,189 @@ +# BinaryStorage: TLA+ model notes + +This model covers binary-model storage in `MonitoredClusteringBuilderState` (MCBS): the storage executor, the shared source-level URI set, and the `ParallelResourceLoader` (PRL) jobs of the current and next cluster. Everything was checked with TLC (`formal/.tools/tla2tools.jar`). + +- MCBS: `com.avaloq.tools.ddk.xtext.builder/src/com/avaloq/tools/ddk/xtext/builder/MonitoredClusteringBuilderState.java` +- PRL: `com.avaloq.tools.ddk.xtext.builder/src/com/avaloq/tools/ddk/xtext/builder/resourceloader/ParallelResourceLoader.java` +- DLRSF: `com.avaloq.tools.ddk.xtext/src/com/avaloq/tools/ddk/xtext/resource/persistence/DirectLinkingResourceStorageFacade.java` +- Xtext 2.44 classes read from the source and bytecode jars in `~/.m2`: `SourceLevelURICache`, `SourceLevelURIsAdapter`, `ResourceStorageFacade`, `StorageAwareResource`, `PortableURIs`, `AbstractResourceLoader`. + +PRL findings F1-F3 (poll timeout counter, interrupt livelock, worker leak) are known and are not modelled here. + +## Files + +| File | What | +|---|---| +| `BinaryStorage.tla` | 488 lines, about 380 non-comment. With every `Fix*`/`Plant*` flag FALSE it is the code as written. | +| `MC.tla` | Size definitions S, M, L and R. A cfg file cannot write sequences or functions. | +| `gen.sh`, `run.sh`, `check_all.sh`, `check_all.out` | Generate the cfgs, run TLC, run the whole matrix, and the results of the last run. | +| `trace.py` | Reads TLC output on stdin and prints only the variables that changed at each step. | + +Sizes (`Clusters`, `Deps`): + +| Size | Clusters | Dependencies | +|---|---|---| +| S | `<<{a},{b}>>` | b→a | +| M | `<<{a1,a2},{b}>>` | a2→a1, b→{a1,a2} | +| L | `<<{a1,a2},{b},{c}>>` | a2→a1, b→a1, c→b | +| R | `<<{a1,a2,a3},{b}>>` | b→a1. With NStore=1 and QCap=1 this fills the executor and reaches CallerRunsPolicy. | + +## What is modelled + +- **Builder thread**, one step per code step: + - `next()`/`addResource` and the queue removal (MCBS:553-556); + - linking loads dependencies into the builder's resource set, and asks `shouldLoadFromStorage`, which reads the sources set (MCBS:569); + - the outer catch for a failed load (MCBS:595-613) and for a link exception after `addResource` (MCBS:608); + - `storeBinaryResource` → `ThreadPoolExecutor.execute` (MCBS:716-736). The executor semantics are: a core thread is started while fewer than NStore exist, then the task goes into the bounded queue, and when the queue is full `CallerRunsPolicy` runs the task on the builder thread. After `shutdown`, `CallerRunsPolicy` discards the task silently. + - `sources.remove(changedURI)` (MCBS:656); + - `loadOperation.cancel()`, then `queueAffectedResources` with `queueURI` and `sources.add` (MCBS:1296-1298, 1312-1314); + - the next load operation, `load(queue)` (MCBS:667-670), which starts **before** `clearResourceSet` (MCBS:672-674); + - `awaitBinaryStorageExecutorTermination` (MCBS:819-874): `shutdown`, `awaitTermination`, then either a timeout or `InterruptedException`. With `retryCount` 0 either one leads to `shutdownNow` (MCBS:877-881), which drops the queued tasks (reported only as a count) and interrupts the workers. A new executor is then created (MCBS:871). + - clearing the resource set (MCBS:1207); the same await also runs in `finally` (MCBS:684). +- **Storage workers**: `doStoreBinaryResource` (MCBS:746-769), split into: + - serialise the resource in memory (this reads the resource and its resource set); + - `fsa.generateFile`: the binary is `partial`, then `new`. If the resource has errors, `deleteStorage` makes the binary `none` (DLRSF:72-76). An interrupted write can throw: the facade then deletes the storage and rethrows, and the error is logged (DLRSF:77-79, MCBS:765); + - `sources.remove(uri)` (MCBS:754). +- **PRL jobs**, one per queued URI: `localResourceSet.getResource(u, true)` (PRL:344-349 → AbstractResourceLoader). + - Every `StorageAwareResource.load` asks `shouldLoadFromStorage` = `!sources.contains(uri) && storageExists`. + - PRL installs the builder's live sources set into each job's resource set without copying it (PRL:168-174). + - `LoaderLoadsDeps` controls whether loading u also loads u's dependencies. PRL:131-137 unloads the extra resources such loads leave behind, so the code expects them to happen. +- **Shared sources set**: the type is `java.util.HashSet`. The bytecode shows `SourceLevelURICache.` calling `Sets.newHashSet()`. `setSourceLevelUrisWithoutCopy` wraps it in `Collections.unmodifiableSet`, which is a view, not a copy (MCBS:1536, PRL:174). Every access is modelled as two steps, begin and end. A mutation that overlaps any other thread's access is the hazard state. +- **Binary file per URI**: `old` (left by the previous build), `none`, `partial` (being written) or `new`. +- **Environment**: at most `MaxTimeouts` await timeouts or interrupts; loader load failures (`AllowLoadFail`); link exceptions (`AllowLinkFail`). +- **Fairness**: weak fairness on each thread's steps, and none on timeouts. + +**Not modelled:** the PRL result queue, counters and cancellation (covered by the earlier model); the order the sorter imposes (the model covers every order); deleted resources (`toBeDeleted`, `deleteBinaryResources`); what a corrupted HashSet actually does (only the overlap is flagged); an Error in a store. + +## Properties + +| Name | Meaning | +|---|---| +| `NotSourceOnlyWhenStored` (P1) | A URI rebuilt in this build leaves `sources` only after its store has finished, with the binary either `new` or deleted. The store must not be queued, dropped, skipped, or still serialising or writing. | +| `StoresAccounted` (P2a) | At `done`, no store is still queued and none was silently discarded. | +| `StoreResolved` (P2b, liveness) | Every queued or running store eventually ends as `ok`, `failed` (logged) or `dropped` (counted by `shutdownNow`). | +| `LoaderNoPartialRead` (P3) | PRL jobs never open a binary that is still being written. | +| `MainNoPartialRead` (P3') | Same check for the builder thread while it links. | +| `NoStaleRead` (P3'') | Nobody opens the previous build's binary of a resource that is being rebuilt in this build. | +| `SetThreadSafe` (P4) | While one thread mutates the HashSet, no other thread accesses it. Two refinements classify the overlaps: `NoReadDuringWrite` and `NoAddDuringRemove`. | +| `NoDetachedStore` (P6) | A store never serialises a resource that is no longer in the builder's resource set. This is the hazard the comment at MCBS:1203 names. | +| `BuildTerminates`, `WorkersQuiesce` (P5, liveness) | The build finishes, and all storage workers eventually stop running. | +| `Witness*` | Invariants that must be violated. They show that each good path is reachable: the build finishes, a second cluster runs, CallerRuns happens, a timeout happens, a `new` binary is read, and a store completes. | + +## Results + +The complete output is in `check_all.out`. The whole matrix took about 11 min wall time on this machine, plus 8m45s for `orig_live_M`. + +| Run | Result | +|---|---| +| The code as written, S | P1, P3, P3', P3'', P4 and P6 are **violated**. P2a, P2b and P5 pass (62,148 distinct states). | +| The code as written, M, liveness (LoadFail and LinkFail off) | P2b and P5 pass (3,859,440 distinct states, 8m45s). | +| Happy environment, M (no timeouts or failures, loaders do not load dependencies) | P1 and P4 are still **violated**. P3, P3', P3'' and P6 pass (15,188 distinct states). | +| Fixed model (FixA-D), all environment options on | All safety and liveness properties pass: S 4.5k, M 364k, M with NStore=2 561k, L 1.72M (4 min), R 911k distinct states. L with NStore=2 and 2 timeouts (2.75M) was checked for safety only. | +| Fixed model with one fix undone | Undoing A → P1 fails. B → P4 fails. C → P6 fails. D → P6 fails. So every fix is needed. | +| Planted bug (a worker removes the URI from sources before writing) | P1 is caught (154 distinct states). | +| Witnesses | All 6 are violated, as intended, in both the original and the fixed model. | + +## Findings + +Traces are the BFS-shortest ones from `./run.sh cfg/.cfg | ./trace.py`. + +### B1: The builder removes a URI from `sources` before its binary is written. CONFIRMED. Violates P1 and causes B2 and B3. + +Trace `orig_P1_nofail` (9 states), with no environment faults needed: + +1. The PRL job loads `a`, and `next()` returns it (MCBS:553-556). +2. `Link` (MCBS:569). +3. `Submit`: `storeBinaryResource` hands the task to a storage thread (MCBS:726). The task is now running or queued. +4. `RmSrc`: `getSources().remove(a)` runs **immediately** (MCBS:656). `a` is now "binary-loadable" while its store is still queued or writing. + +The worker's own `remove` after `saveResource` (MCBS:753-754) is the correct one. MCBS:656 defeats it. + +Checking this against the Java code: MCBS:654 submits the task asynchronously and MCBS:656 runs right after on the builder thread. The same line also removes URIs that were never stored, and that gives a second variant (`orig_NotSourceOnlyWhenStored`, 7 states): +- a PRL load fails, so `LoadOperationException(uri)` sets `changedURI` (MCBS:596); +- `resource` stays null, so no store happens (MCBS:654); +- the URI is still removed from `sources` (MCBS:656), and its **previous build's binary** stays on disk and becomes loadable. + +Upstream Xtext never removes URIs from the source set. It reinstalls a copy per cluster (ClusteringBuilderState.installSourceLevelURIs). + +### B2: The next cluster's loaders read a binary that is being written, or the stale one. CONFIRMED, given that loading u also loads u's dependencies. + +Trace `orig_LoaderNoPartialRead` (19 states): + +1. Cluster 1 processes `a`: `Submit` (MCBS:726), then `RmSrc` (MCBS:656), so `sources = {}`. +2. `EndCluster`, then `QA`: `b` is queued and added to `sources` (MCBS:1297-1298). +3. `NewLoad`: `loadOperation.load(queue)` (MCBS:668-669) starts b's PRL job **before** `clearResourceSet` awaits the storage executor (MCBS:673, 1204). +4. `WSer`, then `WWrite`: `fsa.generateFile` for `a` starts, so `binary[a] = partial`. +5. The PRL job loads `b`, which pulls in dependency `a`. `shouldLoadFromStorage(a)`: `a` is not in `sources` and a storage file exists, so the job opens a's **partial** binary. + +The M trace `orig_loaderpartial_M` (13 states) shows the same thing **within one cluster**: +- a1's store is writing and a1 has already been removed at MCBS:656; +- a2's PRL job, which is still running concurrently, loads dependency a1 from the partial binary. + +`orig_NoStaleRead` (17 states) is the same schedule, but the read happens before the worker starts writing. The job then loads the **previous build's** binary of `a`, even though `a` is being rebuilt. The same happens in the load-failure variant of B1, where a's old binary is never replaced. + +Checking this against the Java code: PRL:168/174 share the live set. `StorageAwareResource.load` → `ResourceStorageFacade.shouldLoadFromStorage` → `doesStorageExist`, then `getOrCreateResourceStorageLoadable` opens the file. +- A truncated read throws `IOException`, and `load` then falls back to the source (`clearAndUnload()` + `super.load`). That costs time but gives the right result. +- A `RuntimeIOException` escapes and fails the load. +- A read of the old binary is silently wrong: the resource is linked against the previous version of a resource that is being rebuilt. + +The trigger needs a PRL load of u to also load another resource. PRL:131-137 exists precisely to unload such extra resources, so this does happen in practice. How often depends on the language: derived state or inference that touches other resources during load. + +Removing MCBS:656 (FixA) closes both the partial and the stale window. Ordering the await before `load(queue)` would only close the next-cluster case, not the within-cluster one. + +### B3: After an await timeout or interrupt, the builder reads a partial binary and clears resources that are still being serialised. CONFIRMED. Violates P3' and P6. + +Trace `orig_mainpartial` (26 states): + +1. `a` is stored asynchronously and removed from `sources` (MCBS:726, 656). +2. `clearResourceSet` → await: `shutdown` (MCBS:826). `AwTimeout` covers `awaitTermination` returning false after 1 min (with `retryCount` 0 the loop exits), or an `InterruptedException`. Both lead to `shutdownNow` (MCBS:837-867, 879). The running task is **not** stopped: an interrupt does not abort in-memory serialisation. +3. `AwDone`: a new executor is created (MCBS:871) and the resource set is cleared (MCBS:1207), while the old worker is still serialising `a`. This is `orig_NoDetachedStore` (19 states, P6). +4. Cluster 2: linking `b` loads `a`. `a` is not in `sources`, and `WWrite` has just made a's binary `partial`, so the builder opens the **partial** binary. + +Checking this against the Java code: +- MCBS:1203 says "this is important as otherwise the resources would unexpectedly become detached from the resource set". The timeout path breaks exactly that guarantee. +- Serialising a detached or cleared resource reaches `PortableURIs.toPortableURI`, which calls `sourceResource.getResourceSet().getEObject(...)` (PortableURIs:183). With the resource set null or cleared, this throws a `NullPointerException` or returns null. +- DLRSF:77-79 then deletes the storage and the failure is logged at MCBS:765. That is benign. The remaining risk is a binary with non-portable references written from a half-cleared set. + +The trigger is a store batch that takes more than 1 minute, or an interrupted build thread. Separately, the catch at MCBS:865-867 swallows `InterruptedException` without re-interrupting the thread. + +### B4: Linking throws, and the resource is removed from the set but still stored. CONFIRMED, low severity. Violates P6. + +Trace `orig_NoDetachedStore` with `AllowLinkFail` (8 states): +1. An exception is thrown after `addResource`, and the outer catch runs `resourceSet.getResources().remove(resource)` (MCBS:608). +2. Execution falls through to `storeBinaryResource(resource, …)` (MCBS:654). +3. The worker serialises a resource whose `getResourceSet()` is null. + +Checking this against the Java code: `resource` is non-null on this path and nothing guards MCBS:654. The outcome is the same as the detached case in B3, most likely an NPE that is logged and the storage deleted. The practical impact is mostly log noise, plus the deletion of a binary that was valid. + +### B5: The HashSet is mutated concurrently by up to three threads without synchronisation. CONFIRMED. Violates P4, even in the happy environment. + +Traces: +- `orig_SetThreadSafe` (11 states): the builder's `remove(a)` (MCBS:656) overlaps the worker's `remove(a)` (MCBS:754). +- `orig_adr` (15 states): the builder's `sources.add(b)` in `queueAffectedResources` (MCBS:1298) overlaps the worker's `remove(a)` (MCBS:754). +- `orig_rdw` (19 states): a PRL job's `contains()`, reached through `shouldLoadFromStorage`, overlaps the worker's `remove` (MCBS:754). + +Checking this against the Java code: +- The set is a plain `HashSet` (bytecode of `SourceLevelURICache.`), shared without copying with the storage threads and every PRL job thread (MCBS:1536, PRL:168-174). +- `update` is `synchronized`, but only the builder thread takes that lock. No other lock is involved. +- Under the Java memory model these are data races. With `HashMap` they can lose an `add`: a queued URI is then missing from `sources`, and its stale binary is loaded instead of the source. That is the bad direction. They can also lose a `remove` (harmless), make `size` wrong, or let a `contains()` miss an entry during a resize. + +The model only flags the overlap. It does not simulate how the `HashMap` gets corrupted. + +### P2 (stores accounted) and P5 (termination) hold. + +- `CallerRunsPolicy` never throws. A discard after `shutdown` is unreachable, because the builder never submits between MCBS:826 and MCBS:871. So the `RejectedExecutionException` catch at MCBS:727-734 is dead code in practice. +- Tasks dropped by `shutdownNow` are reported only as a count, with no URIs. +- Orphaned running tasks finish, under fairness. + +## Minimal fixes in the fixed model + +| Fix | Change | What it resolves | +|---|---|---| +| A | Delete MCBS:656. MCBS:754 already removes the URI once the binary is saved; on the `CallerRunsPolicy` path the builder does this itself. | B1, B2 | +| B | Make the sources set thread-safe, for example by installing `ConcurrentHashMap.newKeySet()` contents via the adapter. `SourceLevelURICache` itself is Xtext-owned. Alternatively, confine all mutations to the builder thread. | B5 | +| C | After `shutdownNow`, keep waiting until the running tasks have finished before clearing or continuing. The trade-off: a truly hung store now blocks the build. | B3 | +| D | Skip `storeBinaryResource` when the outer catch ran, for example by setting `resource = null` after MCBS:608. | B4 | + +## Wall time + +About 40 min of modelling and checking (14:29 to 15:01 for the model and the matrix), plus the 8m45s liveness rerun at size M. diff --git a/formal/binary-storage/tla/cfg/ablateA.cfg b/formal/binary-storage/tla/cfg/ablateA.cfg new file mode 100644 index 000000000..7652e190a --- /dev/null +++ b/formal/binary-storage/tla/cfg/ablateA.cfg @@ -0,0 +1,25 @@ +CONSTANTS + Clusters <- ClustersM + Deps <- DepsM + NStore = 1 + QCap = 1 + MaxTimeouts = 1 + LoaderLoadsDeps = TRUE + AllowLoadFail = TRUE + AllowLinkFail = TRUE + FixA = FALSE + FixB = TRUE + FixC = TRUE + FixD = TRUE + PlantBug = FALSE +SPECIFICATION Spec +INVARIANT TypeOK +INVARIANT TypeOK +INVARIANT NotSourceOnlyWhenStored +INVARIANT StoresAccounted +INVARIANT LoaderNoPartialRead +INVARIANT MainNoPartialRead +INVARIANT NoStaleRead +INVARIANT SetThreadSafe +INVARIANT NoDetachedStore +CHECK_DEADLOCK FALSE diff --git a/formal/binary-storage/tla/cfg/ablateB.cfg b/formal/binary-storage/tla/cfg/ablateB.cfg new file mode 100644 index 000000000..219261fa8 --- /dev/null +++ b/formal/binary-storage/tla/cfg/ablateB.cfg @@ -0,0 +1,25 @@ +CONSTANTS + Clusters <- ClustersM + Deps <- DepsM + NStore = 1 + QCap = 1 + MaxTimeouts = 1 + LoaderLoadsDeps = TRUE + AllowLoadFail = TRUE + AllowLinkFail = TRUE + FixA = TRUE + FixB = FALSE + FixC = TRUE + FixD = TRUE + PlantBug = FALSE +SPECIFICATION Spec +INVARIANT TypeOK +INVARIANT TypeOK +INVARIANT NotSourceOnlyWhenStored +INVARIANT StoresAccounted +INVARIANT LoaderNoPartialRead +INVARIANT MainNoPartialRead +INVARIANT NoStaleRead +INVARIANT SetThreadSafe +INVARIANT NoDetachedStore +CHECK_DEADLOCK FALSE diff --git a/formal/binary-storage/tla/cfg/ablateC.cfg b/formal/binary-storage/tla/cfg/ablateC.cfg new file mode 100644 index 000000000..7811f7aa6 --- /dev/null +++ b/formal/binary-storage/tla/cfg/ablateC.cfg @@ -0,0 +1,25 @@ +CONSTANTS + Clusters <- ClustersM + Deps <- DepsM + NStore = 1 + QCap = 1 + MaxTimeouts = 1 + LoaderLoadsDeps = TRUE + AllowLoadFail = TRUE + AllowLinkFail = TRUE + FixA = TRUE + FixB = TRUE + FixC = FALSE + FixD = TRUE + PlantBug = FALSE +SPECIFICATION Spec +INVARIANT TypeOK +INVARIANT TypeOK +INVARIANT NotSourceOnlyWhenStored +INVARIANT StoresAccounted +INVARIANT LoaderNoPartialRead +INVARIANT MainNoPartialRead +INVARIANT NoStaleRead +INVARIANT SetThreadSafe +INVARIANT NoDetachedStore +CHECK_DEADLOCK FALSE diff --git a/formal/binary-storage/tla/cfg/ablateD.cfg b/formal/binary-storage/tla/cfg/ablateD.cfg new file mode 100644 index 000000000..31d534497 --- /dev/null +++ b/formal/binary-storage/tla/cfg/ablateD.cfg @@ -0,0 +1,25 @@ +CONSTANTS + Clusters <- ClustersM + Deps <- DepsM + NStore = 1 + QCap = 1 + MaxTimeouts = 1 + LoaderLoadsDeps = TRUE + AllowLoadFail = TRUE + AllowLinkFail = TRUE + FixA = TRUE + FixB = TRUE + FixC = TRUE + FixD = FALSE + PlantBug = FALSE +SPECIFICATION Spec +INVARIANT TypeOK +INVARIANT TypeOK +INVARIANT NotSourceOnlyWhenStored +INVARIANT StoresAccounted +INVARIANT LoaderNoPartialRead +INVARIANT MainNoPartialRead +INVARIANT NoStaleRead +INVARIANT SetThreadSafe +INVARIANT NoDetachedStore +CHECK_DEADLOCK FALSE diff --git a/formal/binary-storage/tla/cfg/fixed_L.cfg b/formal/binary-storage/tla/cfg/fixed_L.cfg new file mode 100644 index 000000000..d2f0f868e --- /dev/null +++ b/formal/binary-storage/tla/cfg/fixed_L.cfg @@ -0,0 +1,28 @@ +CONSTANTS + Clusters <- ClustersL + Deps <- DepsL + NStore = 1 + QCap = 1 + MaxTimeouts = 1 + LoaderLoadsDeps = TRUE + AllowLoadFail = TRUE + AllowLinkFail = TRUE + FixA = TRUE + FixB = TRUE + FixC = TRUE + FixD = TRUE + PlantBug = FALSE +SPECIFICATION Spec +INVARIANT TypeOK +INVARIANT TypeOK +INVARIANT NotSourceOnlyWhenStored +INVARIANT StoresAccounted +INVARIANT LoaderNoPartialRead +INVARIANT MainNoPartialRead +INVARIANT NoStaleRead +INVARIANT SetThreadSafe +INVARIANT NoDetachedStore +PROPERTY BuildTerminates +PROPERTY WorkersQuiesce +PROPERTY StoreResolved +CHECK_DEADLOCK FALSE diff --git a/formal/binary-storage/tla/cfg/fixed_L2.cfg b/formal/binary-storage/tla/cfg/fixed_L2.cfg new file mode 100644 index 000000000..fd4ac5ab0 --- /dev/null +++ b/formal/binary-storage/tla/cfg/fixed_L2.cfg @@ -0,0 +1,25 @@ +CONSTANTS + Clusters <- ClustersL + Deps <- DepsL + NStore = 2 + QCap = 1 + MaxTimeouts = 2 + LoaderLoadsDeps = TRUE + AllowLoadFail = TRUE + AllowLinkFail = TRUE + FixA = TRUE + FixB = TRUE + FixC = TRUE + FixD = TRUE + PlantBug = FALSE +SPECIFICATION Spec +INVARIANT TypeOK +INVARIANT TypeOK +INVARIANT NotSourceOnlyWhenStored +INVARIANT StoresAccounted +INVARIANT LoaderNoPartialRead +INVARIANT MainNoPartialRead +INVARIANT NoStaleRead +INVARIANT SetThreadSafe +INVARIANT NoDetachedStore +CHECK_DEADLOCK FALSE diff --git a/formal/binary-storage/tla/cfg/fixed_M.cfg b/formal/binary-storage/tla/cfg/fixed_M.cfg new file mode 100644 index 000000000..e83d08db8 --- /dev/null +++ b/formal/binary-storage/tla/cfg/fixed_M.cfg @@ -0,0 +1,28 @@ +CONSTANTS + Clusters <- ClustersM + Deps <- DepsM + NStore = 1 + QCap = 1 + MaxTimeouts = 1 + LoaderLoadsDeps = TRUE + AllowLoadFail = TRUE + AllowLinkFail = TRUE + FixA = TRUE + FixB = TRUE + FixC = TRUE + FixD = TRUE + PlantBug = FALSE +SPECIFICATION Spec +INVARIANT TypeOK +INVARIANT TypeOK +INVARIANT NotSourceOnlyWhenStored +INVARIANT StoresAccounted +INVARIANT LoaderNoPartialRead +INVARIANT MainNoPartialRead +INVARIANT NoStaleRead +INVARIANT SetThreadSafe +INVARIANT NoDetachedStore +PROPERTY BuildTerminates +PROPERTY WorkersQuiesce +PROPERTY StoreResolved +CHECK_DEADLOCK FALSE diff --git a/formal/binary-storage/tla/cfg/fixed_M2.cfg b/formal/binary-storage/tla/cfg/fixed_M2.cfg new file mode 100644 index 000000000..7b1d5ea1f --- /dev/null +++ b/formal/binary-storage/tla/cfg/fixed_M2.cfg @@ -0,0 +1,28 @@ +CONSTANTS + Clusters <- ClustersM + Deps <- DepsM + NStore = 2 + QCap = 1 + MaxTimeouts = 1 + LoaderLoadsDeps = TRUE + AllowLoadFail = TRUE + AllowLinkFail = TRUE + FixA = TRUE + FixB = TRUE + FixC = TRUE + FixD = TRUE + PlantBug = FALSE +SPECIFICATION Spec +INVARIANT TypeOK +INVARIANT TypeOK +INVARIANT NotSourceOnlyWhenStored +INVARIANT StoresAccounted +INVARIANT LoaderNoPartialRead +INVARIANT MainNoPartialRead +INVARIANT NoStaleRead +INVARIANT SetThreadSafe +INVARIANT NoDetachedStore +PROPERTY BuildTerminates +PROPERTY WorkersQuiesce +PROPERTY StoreResolved +CHECK_DEADLOCK FALSE diff --git a/formal/binary-storage/tla/cfg/fixed_R.cfg b/formal/binary-storage/tla/cfg/fixed_R.cfg new file mode 100644 index 000000000..4514989b5 --- /dev/null +++ b/formal/binary-storage/tla/cfg/fixed_R.cfg @@ -0,0 +1,28 @@ +CONSTANTS + Clusters <- ClustersR + Deps <- DepsR + NStore = 1 + QCap = 1 + MaxTimeouts = 1 + LoaderLoadsDeps = TRUE + AllowLoadFail = TRUE + AllowLinkFail = TRUE + FixA = TRUE + FixB = TRUE + FixC = TRUE + FixD = TRUE + PlantBug = FALSE +SPECIFICATION Spec +INVARIANT TypeOK +INVARIANT TypeOK +INVARIANT NotSourceOnlyWhenStored +INVARIANT StoresAccounted +INVARIANT LoaderNoPartialRead +INVARIANT MainNoPartialRead +INVARIANT NoStaleRead +INVARIANT SetThreadSafe +INVARIANT NoDetachedStore +PROPERTY BuildTerminates +PROPERTY WorkersQuiesce +PROPERTY StoreResolved +CHECK_DEADLOCK FALSE diff --git a/formal/binary-storage/tla/cfg/fixed_S.cfg b/formal/binary-storage/tla/cfg/fixed_S.cfg new file mode 100644 index 000000000..c2681d8ae --- /dev/null +++ b/formal/binary-storage/tla/cfg/fixed_S.cfg @@ -0,0 +1,28 @@ +CONSTANTS + Clusters <- ClustersS + Deps <- DepsS + NStore = 1 + QCap = 1 + MaxTimeouts = 1 + LoaderLoadsDeps = TRUE + AllowLoadFail = TRUE + AllowLinkFail = TRUE + FixA = TRUE + FixB = TRUE + FixC = TRUE + FixD = TRUE + PlantBug = FALSE +SPECIFICATION Spec +INVARIANT TypeOK +INVARIANT TypeOK +INVARIANT NotSourceOnlyWhenStored +INVARIANT StoresAccounted +INVARIANT LoaderNoPartialRead +INVARIANT MainNoPartialRead +INVARIANT NoStaleRead +INVARIANT SetThreadSafe +INVARIANT NoDetachedStore +PROPERTY BuildTerminates +PROPERTY WorkersQuiesce +PROPERTY StoreResolved +CHECK_DEADLOCK FALSE diff --git a/formal/binary-storage/tla/cfg/happy_LoaderNoPartialRead.cfg b/formal/binary-storage/tla/cfg/happy_LoaderNoPartialRead.cfg new file mode 100644 index 000000000..6015ba0ae --- /dev/null +++ b/formal/binary-storage/tla/cfg/happy_LoaderNoPartialRead.cfg @@ -0,0 +1,18 @@ +CONSTANTS + Clusters <- ClustersM + Deps <- DepsM + NStore = 2 + QCap = 1 + MaxTimeouts = 0 + LoaderLoadsDeps = FALSE + AllowLoadFail = FALSE + AllowLinkFail = FALSE + FixA = FALSE + FixB = FALSE + FixC = FALSE + FixD = FALSE + PlantBug = FALSE +SPECIFICATION Spec +INVARIANT TypeOK +INVARIANT LoaderNoPartialRead +CHECK_DEADLOCK FALSE diff --git a/formal/binary-storage/tla/cfg/happy_MainNoPartialRead.cfg b/formal/binary-storage/tla/cfg/happy_MainNoPartialRead.cfg new file mode 100644 index 000000000..84745f5ea --- /dev/null +++ b/formal/binary-storage/tla/cfg/happy_MainNoPartialRead.cfg @@ -0,0 +1,18 @@ +CONSTANTS + Clusters <- ClustersM + Deps <- DepsM + NStore = 2 + QCap = 1 + MaxTimeouts = 0 + LoaderLoadsDeps = FALSE + AllowLoadFail = FALSE + AllowLinkFail = FALSE + FixA = FALSE + FixB = FALSE + FixC = FALSE + FixD = FALSE + PlantBug = FALSE +SPECIFICATION Spec +INVARIANT TypeOK +INVARIANT MainNoPartialRead +CHECK_DEADLOCK FALSE diff --git a/formal/binary-storage/tla/cfg/happy_NoDetachedStore.cfg b/formal/binary-storage/tla/cfg/happy_NoDetachedStore.cfg new file mode 100644 index 000000000..7ca7eed82 --- /dev/null +++ b/formal/binary-storage/tla/cfg/happy_NoDetachedStore.cfg @@ -0,0 +1,18 @@ +CONSTANTS + Clusters <- ClustersM + Deps <- DepsM + NStore = 2 + QCap = 1 + MaxTimeouts = 0 + LoaderLoadsDeps = FALSE + AllowLoadFail = FALSE + AllowLinkFail = FALSE + FixA = FALSE + FixB = FALSE + FixC = FALSE + FixD = FALSE + PlantBug = FALSE +SPECIFICATION Spec +INVARIANT TypeOK +INVARIANT NoDetachedStore +CHECK_DEADLOCK FALSE diff --git a/formal/binary-storage/tla/cfg/happy_NoStaleRead.cfg b/formal/binary-storage/tla/cfg/happy_NoStaleRead.cfg new file mode 100644 index 000000000..3d3044b0a --- /dev/null +++ b/formal/binary-storage/tla/cfg/happy_NoStaleRead.cfg @@ -0,0 +1,18 @@ +CONSTANTS + Clusters <- ClustersM + Deps <- DepsM + NStore = 2 + QCap = 1 + MaxTimeouts = 0 + LoaderLoadsDeps = FALSE + AllowLoadFail = FALSE + AllowLinkFail = FALSE + FixA = FALSE + FixB = FALSE + FixC = FALSE + FixD = FALSE + PlantBug = FALSE +SPECIFICATION Spec +INVARIANT TypeOK +INVARIANT NoStaleRead +CHECK_DEADLOCK FALSE diff --git a/formal/binary-storage/tla/cfg/happy_NotSourceOnlyWhenStored.cfg b/formal/binary-storage/tla/cfg/happy_NotSourceOnlyWhenStored.cfg new file mode 100644 index 000000000..69f1e4a91 --- /dev/null +++ b/formal/binary-storage/tla/cfg/happy_NotSourceOnlyWhenStored.cfg @@ -0,0 +1,18 @@ +CONSTANTS + Clusters <- ClustersM + Deps <- DepsM + NStore = 2 + QCap = 1 + MaxTimeouts = 0 + LoaderLoadsDeps = FALSE + AllowLoadFail = FALSE + AllowLinkFail = FALSE + FixA = FALSE + FixB = FALSE + FixC = FALSE + FixD = FALSE + PlantBug = FALSE +SPECIFICATION Spec +INVARIANT TypeOK +INVARIANT NotSourceOnlyWhenStored +CHECK_DEADLOCK FALSE diff --git a/formal/binary-storage/tla/cfg/happy_SetThreadSafe.cfg b/formal/binary-storage/tla/cfg/happy_SetThreadSafe.cfg new file mode 100644 index 000000000..09cf51b5a --- /dev/null +++ b/formal/binary-storage/tla/cfg/happy_SetThreadSafe.cfg @@ -0,0 +1,18 @@ +CONSTANTS + Clusters <- ClustersM + Deps <- DepsM + NStore = 2 + QCap = 1 + MaxTimeouts = 0 + LoaderLoadsDeps = FALSE + AllowLoadFail = FALSE + AllowLinkFail = FALSE + FixA = FALSE + FixB = FALSE + FixC = FALSE + FixD = FALSE + PlantBug = FALSE +SPECIFICATION Spec +INVARIANT TypeOK +INVARIANT SetThreadSafe +CHECK_DEADLOCK FALSE diff --git a/formal/binary-storage/tla/cfg/orig_LoaderNoPartialRead.cfg b/formal/binary-storage/tla/cfg/orig_LoaderNoPartialRead.cfg new file mode 100644 index 000000000..8f371a395 --- /dev/null +++ b/formal/binary-storage/tla/cfg/orig_LoaderNoPartialRead.cfg @@ -0,0 +1,18 @@ +CONSTANTS + Clusters <- ClustersS + Deps <- DepsS + NStore = 1 + QCap = 1 + MaxTimeouts = 1 + LoaderLoadsDeps = TRUE + AllowLoadFail = TRUE + AllowLinkFail = TRUE + FixA = FALSE + FixB = FALSE + FixC = FALSE + FixD = FALSE + PlantBug = FALSE +SPECIFICATION Spec +INVARIANT TypeOK +INVARIANT LoaderNoPartialRead +CHECK_DEADLOCK FALSE diff --git a/formal/binary-storage/tla/cfg/orig_MainNoPartialRead.cfg b/formal/binary-storage/tla/cfg/orig_MainNoPartialRead.cfg new file mode 100644 index 000000000..c2377ba41 --- /dev/null +++ b/formal/binary-storage/tla/cfg/orig_MainNoPartialRead.cfg @@ -0,0 +1,18 @@ +CONSTANTS + Clusters <- ClustersS + Deps <- DepsS + NStore = 1 + QCap = 1 + MaxTimeouts = 1 + LoaderLoadsDeps = TRUE + AllowLoadFail = TRUE + AllowLinkFail = TRUE + FixA = FALSE + FixB = FALSE + FixC = FALSE + FixD = FALSE + PlantBug = FALSE +SPECIFICATION Spec +INVARIANT TypeOK +INVARIANT MainNoPartialRead +CHECK_DEADLOCK FALSE diff --git a/formal/binary-storage/tla/cfg/orig_NoDetachedStore.cfg b/formal/binary-storage/tla/cfg/orig_NoDetachedStore.cfg new file mode 100644 index 000000000..39b7000c4 --- /dev/null +++ b/formal/binary-storage/tla/cfg/orig_NoDetachedStore.cfg @@ -0,0 +1,18 @@ +CONSTANTS + Clusters <- ClustersS + Deps <- DepsS + NStore = 1 + QCap = 1 + MaxTimeouts = 1 + LoaderLoadsDeps = TRUE + AllowLoadFail = TRUE + AllowLinkFail = TRUE + FixA = FALSE + FixB = FALSE + FixC = FALSE + FixD = FALSE + PlantBug = FALSE +SPECIFICATION Spec +INVARIANT TypeOK +INVARIANT NoDetachedStore +CHECK_DEADLOCK FALSE diff --git a/formal/binary-storage/tla/cfg/orig_NoStaleRead.cfg b/formal/binary-storage/tla/cfg/orig_NoStaleRead.cfg new file mode 100644 index 000000000..0f1c3fe3b --- /dev/null +++ b/formal/binary-storage/tla/cfg/orig_NoStaleRead.cfg @@ -0,0 +1,18 @@ +CONSTANTS + Clusters <- ClustersS + Deps <- DepsS + NStore = 1 + QCap = 1 + MaxTimeouts = 1 + LoaderLoadsDeps = TRUE + AllowLoadFail = TRUE + AllowLinkFail = TRUE + FixA = FALSE + FixB = FALSE + FixC = FALSE + FixD = FALSE + PlantBug = FALSE +SPECIFICATION Spec +INVARIANT TypeOK +INVARIANT NoStaleRead +CHECK_DEADLOCK FALSE diff --git a/formal/binary-storage/tla/cfg/orig_NotSourceOnlyWhenStored.cfg b/formal/binary-storage/tla/cfg/orig_NotSourceOnlyWhenStored.cfg new file mode 100644 index 000000000..11fa8a03c --- /dev/null +++ b/formal/binary-storage/tla/cfg/orig_NotSourceOnlyWhenStored.cfg @@ -0,0 +1,18 @@ +CONSTANTS + Clusters <- ClustersS + Deps <- DepsS + NStore = 1 + QCap = 1 + MaxTimeouts = 1 + LoaderLoadsDeps = TRUE + AllowLoadFail = TRUE + AllowLinkFail = TRUE + FixA = FALSE + FixB = FALSE + FixC = FALSE + FixD = FALSE + PlantBug = FALSE +SPECIFICATION Spec +INVARIANT TypeOK +INVARIANT NotSourceOnlyWhenStored +CHECK_DEADLOCK FALSE diff --git a/formal/binary-storage/tla/cfg/orig_P1_nofail.cfg b/formal/binary-storage/tla/cfg/orig_P1_nofail.cfg new file mode 100644 index 000000000..aa1cf56a7 --- /dev/null +++ b/formal/binary-storage/tla/cfg/orig_P1_nofail.cfg @@ -0,0 +1,18 @@ +CONSTANTS + Clusters <- ClustersS + Deps <- DepsS + NStore = 1 + QCap = 1 + MaxTimeouts = 0 + LoaderLoadsDeps = FALSE + AllowLoadFail = FALSE + AllowLinkFail = FALSE + FixA = FALSE + FixB = FALSE + FixC = FALSE + FixD = FALSE + PlantBug = FALSE +SPECIFICATION Spec +INVARIANT TypeOK +INVARIANT NotSourceOnlyWhenStored +CHECK_DEADLOCK FALSE diff --git a/formal/binary-storage/tla/cfg/orig_SetThreadSafe.cfg b/formal/binary-storage/tla/cfg/orig_SetThreadSafe.cfg new file mode 100644 index 000000000..fe4ab66a4 --- /dev/null +++ b/formal/binary-storage/tla/cfg/orig_SetThreadSafe.cfg @@ -0,0 +1,18 @@ +CONSTANTS + Clusters <- ClustersS + Deps <- DepsS + NStore = 1 + QCap = 1 + MaxTimeouts = 1 + LoaderLoadsDeps = TRUE + AllowLoadFail = TRUE + AllowLinkFail = TRUE + FixA = FALSE + FixB = FALSE + FixC = FALSE + FixD = FALSE + PlantBug = FALSE +SPECIFICATION Spec +INVARIANT TypeOK +INVARIANT SetThreadSafe +CHECK_DEADLOCK FALSE diff --git a/formal/binary-storage/tla/cfg/orig_StoresAccounted.cfg b/formal/binary-storage/tla/cfg/orig_StoresAccounted.cfg new file mode 100644 index 000000000..818ab4fe9 --- /dev/null +++ b/formal/binary-storage/tla/cfg/orig_StoresAccounted.cfg @@ -0,0 +1,18 @@ +CONSTANTS + Clusters <- ClustersS + Deps <- DepsS + NStore = 1 + QCap = 1 + MaxTimeouts = 1 + LoaderLoadsDeps = TRUE + AllowLoadFail = TRUE + AllowLinkFail = TRUE + FixA = FALSE + FixB = FALSE + FixC = FALSE + FixD = FALSE + PlantBug = FALSE +SPECIFICATION Spec +INVARIANT TypeOK +INVARIANT StoresAccounted +CHECK_DEADLOCK FALSE diff --git a/formal/binary-storage/tla/cfg/orig_TypeOK.cfg b/formal/binary-storage/tla/cfg/orig_TypeOK.cfg new file mode 100644 index 000000000..a3c7ed903 --- /dev/null +++ b/formal/binary-storage/tla/cfg/orig_TypeOK.cfg @@ -0,0 +1,18 @@ +CONSTANTS + Clusters <- ClustersS + Deps <- DepsS + NStore = 1 + QCap = 1 + MaxTimeouts = 1 + LoaderLoadsDeps = TRUE + AllowLoadFail = TRUE + AllowLinkFail = TRUE + FixA = FALSE + FixB = FALSE + FixC = FALSE + FixD = FALSE + PlantBug = FALSE +SPECIFICATION Spec +INVARIANT TypeOK +INVARIANT TypeOK +CHECK_DEADLOCK FALSE diff --git a/formal/binary-storage/tla/cfg/orig_adr.cfg b/formal/binary-storage/tla/cfg/orig_adr.cfg new file mode 100644 index 000000000..b8182c28e --- /dev/null +++ b/formal/binary-storage/tla/cfg/orig_adr.cfg @@ -0,0 +1,18 @@ +CONSTANTS + Clusters <- ClustersS + Deps <- DepsS + NStore = 1 + QCap = 1 + MaxTimeouts = 1 + LoaderLoadsDeps = TRUE + AllowLoadFail = FALSE + AllowLinkFail = FALSE + FixA = FALSE + FixB = FALSE + FixC = FALSE + FixD = FALSE + PlantBug = FALSE +SPECIFICATION Spec +INVARIANT TypeOK +INVARIANT NoAddDuringRemove +CHECK_DEADLOCK FALSE diff --git a/formal/binary-storage/tla/cfg/orig_detached_nolinkfail.cfg b/formal/binary-storage/tla/cfg/orig_detached_nolinkfail.cfg new file mode 100644 index 000000000..96536e1d4 --- /dev/null +++ b/formal/binary-storage/tla/cfg/orig_detached_nolinkfail.cfg @@ -0,0 +1,18 @@ +CONSTANTS + Clusters <- ClustersS + Deps <- DepsS + NStore = 1 + QCap = 1 + MaxTimeouts = 1 + LoaderLoadsDeps = FALSE + AllowLoadFail = FALSE + AllowLinkFail = FALSE + FixA = FALSE + FixB = FALSE + FixC = FALSE + FixD = FALSE + PlantBug = FALSE +SPECIFICATION Spec +INVARIANT TypeOK +INVARIANT NoDetachedStore +CHECK_DEADLOCK FALSE diff --git a/formal/binary-storage/tla/cfg/orig_live.cfg b/formal/binary-storage/tla/cfg/orig_live.cfg new file mode 100644 index 000000000..1d50627fd --- /dev/null +++ b/formal/binary-storage/tla/cfg/orig_live.cfg @@ -0,0 +1,20 @@ +CONSTANTS + Clusters <- ClustersS + Deps <- DepsS + NStore = 1 + QCap = 1 + MaxTimeouts = 1 + LoaderLoadsDeps = TRUE + AllowLoadFail = TRUE + AllowLinkFail = TRUE + FixA = FALSE + FixB = FALSE + FixC = FALSE + FixD = FALSE + PlantBug = FALSE +SPECIFICATION Spec +INVARIANT TypeOK +PROPERTY BuildTerminates +PROPERTY WorkersQuiesce +PROPERTY StoreResolved +CHECK_DEADLOCK FALSE diff --git a/formal/binary-storage/tla/cfg/orig_live_M.cfg b/formal/binary-storage/tla/cfg/orig_live_M.cfg new file mode 100644 index 000000000..823e84ae9 --- /dev/null +++ b/formal/binary-storage/tla/cfg/orig_live_M.cfg @@ -0,0 +1,20 @@ +CONSTANTS + Clusters <- ClustersM + Deps <- DepsM + NStore = 1 + QCap = 1 + MaxTimeouts = 1 + LoaderLoadsDeps = TRUE + AllowLoadFail = FALSE + AllowLinkFail = FALSE + FixA = FALSE + FixB = FALSE + FixC = FALSE + FixD = FALSE + PlantBug = FALSE +SPECIFICATION Spec +INVARIANT TypeOK +PROPERTY BuildTerminates +PROPERTY WorkersQuiesce +PROPERTY StoreResolved +CHECK_DEADLOCK FALSE diff --git a/formal/binary-storage/tla/cfg/orig_loaderpartial_M.cfg b/formal/binary-storage/tla/cfg/orig_loaderpartial_M.cfg new file mode 100644 index 000000000..4db789e17 --- /dev/null +++ b/formal/binary-storage/tla/cfg/orig_loaderpartial_M.cfg @@ -0,0 +1,18 @@ +CONSTANTS + Clusters <- ClustersM + Deps <- DepsM + NStore = 1 + QCap = 1 + MaxTimeouts = 0 + LoaderLoadsDeps = TRUE + AllowLoadFail = FALSE + AllowLinkFail = FALSE + FixA = FALSE + FixB = FALSE + FixC = FALSE + FixD = FALSE + PlantBug = FALSE +SPECIFICATION Spec +INVARIANT TypeOK +INVARIANT LoaderNoPartialRead +CHECK_DEADLOCK FALSE diff --git a/formal/binary-storage/tla/cfg/orig_mainpartial.cfg b/formal/binary-storage/tla/cfg/orig_mainpartial.cfg new file mode 100644 index 000000000..63c1810c2 --- /dev/null +++ b/formal/binary-storage/tla/cfg/orig_mainpartial.cfg @@ -0,0 +1,18 @@ +CONSTANTS + Clusters <- ClustersS + Deps <- DepsS + NStore = 1 + QCap = 1 + MaxTimeouts = 1 + LoaderLoadsDeps = FALSE + AllowLoadFail = FALSE + AllowLinkFail = FALSE + FixA = FALSE + FixB = FALSE + FixC = FALSE + FixD = FALSE + PlantBug = FALSE +SPECIFICATION Spec +INVARIANT TypeOK +INVARIANT MainNoPartialRead +CHECK_DEADLOCK FALSE diff --git a/formal/binary-storage/tla/cfg/orig_rdw.cfg b/formal/binary-storage/tla/cfg/orig_rdw.cfg new file mode 100644 index 000000000..516fda7c1 --- /dev/null +++ b/formal/binary-storage/tla/cfg/orig_rdw.cfg @@ -0,0 +1,18 @@ +CONSTANTS + Clusters <- ClustersS + Deps <- DepsS + NStore = 1 + QCap = 1 + MaxTimeouts = 1 + LoaderLoadsDeps = TRUE + AllowLoadFail = FALSE + AllowLinkFail = FALSE + FixA = FALSE + FixB = FALSE + FixC = FALSE + FixD = FALSE + PlantBug = FALSE +SPECIFICATION Spec +INVARIANT TypeOK +INVARIANT NoReadDuringWrite +CHECK_DEADLOCK FALSE diff --git a/formal/binary-storage/tla/cfg/orig_stale_nofail.cfg b/formal/binary-storage/tla/cfg/orig_stale_nofail.cfg new file mode 100644 index 000000000..ed0d2d3e7 --- /dev/null +++ b/formal/binary-storage/tla/cfg/orig_stale_nofail.cfg @@ -0,0 +1,18 @@ +CONSTANTS + Clusters <- ClustersS + Deps <- DepsS + NStore = 1 + QCap = 1 + MaxTimeouts = 1 + LoaderLoadsDeps = TRUE + AllowLoadFail = FALSE + AllowLinkFail = FALSE + FixA = FALSE + FixB = FALSE + FixC = FALSE + FixD = FALSE + PlantBug = FALSE +SPECIFICATION Spec +INVARIANT TypeOK +INVARIANT NoStaleRead +CHECK_DEADLOCK FALSE diff --git a/formal/binary-storage/tla/cfg/planted.cfg b/formal/binary-storage/tla/cfg/planted.cfg new file mode 100644 index 000000000..dfff5b9cc --- /dev/null +++ b/formal/binary-storage/tla/cfg/planted.cfg @@ -0,0 +1,25 @@ +CONSTANTS + Clusters <- ClustersS + Deps <- DepsS + NStore = 1 + QCap = 1 + MaxTimeouts = 1 + LoaderLoadsDeps = TRUE + AllowLoadFail = TRUE + AllowLinkFail = TRUE + FixA = TRUE + FixB = TRUE + FixC = TRUE + FixD = TRUE + PlantBug = TRUE +SPECIFICATION Spec +INVARIANT TypeOK +INVARIANT TypeOK +INVARIANT NotSourceOnlyWhenStored +INVARIANT StoresAccounted +INVARIANT LoaderNoPartialRead +INVARIANT MainNoPartialRead +INVARIANT NoStaleRead +INVARIANT SetThreadSafe +INVARIANT NoDetachedStore +CHECK_DEADLOCK FALSE diff --git a/formal/binary-storage/tla/cfg/smoke.cfg b/formal/binary-storage/tla/cfg/smoke.cfg new file mode 100644 index 000000000..ce49bf01e --- /dev/null +++ b/formal/binary-storage/tla/cfg/smoke.cfg @@ -0,0 +1,18 @@ +CONSTANTS + Clusters <- ClustersS + Deps <- DepsS + NStore = 1 + QCap = 1 + MaxTimeouts = 1 + LoaderLoadsDeps = TRUE + AllowLoadFail = TRUE + AllowLinkFail = TRUE + FixA = FALSE + FixB = FALSE + FixC = FALSE + FixD = FALSE + PlantBug = FALSE +SPECIFICATION Spec +INVARIANT TypeOK +INVARIANT WitnessDone +CHECK_DEADLOCK FALSE diff --git a/formal/binary-storage/tla/cfg/wit_fixed_WitnessCallerRuns.cfg b/formal/binary-storage/tla/cfg/wit_fixed_WitnessCallerRuns.cfg new file mode 100644 index 000000000..2a8053e4f --- /dev/null +++ b/formal/binary-storage/tla/cfg/wit_fixed_WitnessCallerRuns.cfg @@ -0,0 +1,18 @@ +CONSTANTS + Clusters <- ClustersR + Deps <- DepsR + NStore = 1 + QCap = 1 + MaxTimeouts = 1 + LoaderLoadsDeps = TRUE + AllowLoadFail = TRUE + AllowLinkFail = TRUE + FixA = TRUE + FixB = TRUE + FixC = TRUE + FixD = TRUE + PlantBug = FALSE +SPECIFICATION Spec +INVARIANT TypeOK +INVARIANT WitnessCallerRuns +CHECK_DEADLOCK FALSE diff --git a/formal/binary-storage/tla/cfg/wit_fixed_WitnessDone.cfg b/formal/binary-storage/tla/cfg/wit_fixed_WitnessDone.cfg new file mode 100644 index 000000000..6f7b34257 --- /dev/null +++ b/formal/binary-storage/tla/cfg/wit_fixed_WitnessDone.cfg @@ -0,0 +1,18 @@ +CONSTANTS + Clusters <- ClustersR + Deps <- DepsR + NStore = 1 + QCap = 1 + MaxTimeouts = 1 + LoaderLoadsDeps = TRUE + AllowLoadFail = TRUE + AllowLinkFail = TRUE + FixA = TRUE + FixB = TRUE + FixC = TRUE + FixD = TRUE + PlantBug = FALSE +SPECIFICATION Spec +INVARIANT TypeOK +INVARIANT WitnessDone +CHECK_DEADLOCK FALSE diff --git a/formal/binary-storage/tla/cfg/wit_fixed_WitnessGoodRead.cfg b/formal/binary-storage/tla/cfg/wit_fixed_WitnessGoodRead.cfg new file mode 100644 index 000000000..3f36b3acf --- /dev/null +++ b/formal/binary-storage/tla/cfg/wit_fixed_WitnessGoodRead.cfg @@ -0,0 +1,18 @@ +CONSTANTS + Clusters <- ClustersR + Deps <- DepsR + NStore = 1 + QCap = 1 + MaxTimeouts = 1 + LoaderLoadsDeps = TRUE + AllowLoadFail = TRUE + AllowLinkFail = TRUE + FixA = TRUE + FixB = TRUE + FixC = TRUE + FixD = TRUE + PlantBug = FALSE +SPECIFICATION Spec +INVARIANT TypeOK +INVARIANT WitnessGoodRead +CHECK_DEADLOCK FALSE diff --git a/formal/binary-storage/tla/cfg/wit_fixed_WitnessSecondClust.cfg b/formal/binary-storage/tla/cfg/wit_fixed_WitnessSecondClust.cfg new file mode 100644 index 000000000..b3c5ab046 --- /dev/null +++ b/formal/binary-storage/tla/cfg/wit_fixed_WitnessSecondClust.cfg @@ -0,0 +1,18 @@ +CONSTANTS + Clusters <- ClustersR + Deps <- DepsR + NStore = 1 + QCap = 1 + MaxTimeouts = 1 + LoaderLoadsDeps = TRUE + AllowLoadFail = TRUE + AllowLinkFail = TRUE + FixA = TRUE + FixB = TRUE + FixC = TRUE + FixD = TRUE + PlantBug = FALSE +SPECIFICATION Spec +INVARIANT TypeOK +INVARIANT WitnessSecondClust +CHECK_DEADLOCK FALSE diff --git a/formal/binary-storage/tla/cfg/wit_fixed_WitnessStoreOk.cfg b/formal/binary-storage/tla/cfg/wit_fixed_WitnessStoreOk.cfg new file mode 100644 index 000000000..6a00fd611 --- /dev/null +++ b/formal/binary-storage/tla/cfg/wit_fixed_WitnessStoreOk.cfg @@ -0,0 +1,18 @@ +CONSTANTS + Clusters <- ClustersR + Deps <- DepsR + NStore = 1 + QCap = 1 + MaxTimeouts = 1 + LoaderLoadsDeps = TRUE + AllowLoadFail = TRUE + AllowLinkFail = TRUE + FixA = TRUE + FixB = TRUE + FixC = TRUE + FixD = TRUE + PlantBug = FALSE +SPECIFICATION Spec +INVARIANT TypeOK +INVARIANT WitnessStoreOk +CHECK_DEADLOCK FALSE diff --git a/formal/binary-storage/tla/cfg/wit_fixed_WitnessTimeout.cfg b/formal/binary-storage/tla/cfg/wit_fixed_WitnessTimeout.cfg new file mode 100644 index 000000000..26770ee97 --- /dev/null +++ b/formal/binary-storage/tla/cfg/wit_fixed_WitnessTimeout.cfg @@ -0,0 +1,18 @@ +CONSTANTS + Clusters <- ClustersR + Deps <- DepsR + NStore = 1 + QCap = 1 + MaxTimeouts = 1 + LoaderLoadsDeps = TRUE + AllowLoadFail = TRUE + AllowLinkFail = TRUE + FixA = TRUE + FixB = TRUE + FixC = TRUE + FixD = TRUE + PlantBug = FALSE +SPECIFICATION Spec +INVARIANT TypeOK +INVARIANT WitnessTimeout +CHECK_DEADLOCK FALSE diff --git a/formal/binary-storage/tla/cfg/wit_orig_WitnessCallerRuns.cfg b/formal/binary-storage/tla/cfg/wit_orig_WitnessCallerRuns.cfg new file mode 100644 index 000000000..13dae40e0 --- /dev/null +++ b/formal/binary-storage/tla/cfg/wit_orig_WitnessCallerRuns.cfg @@ -0,0 +1,18 @@ +CONSTANTS + Clusters <- ClustersR + Deps <- DepsR + NStore = 1 + QCap = 1 + MaxTimeouts = 1 + LoaderLoadsDeps = TRUE + AllowLoadFail = TRUE + AllowLinkFail = TRUE + FixA = FALSE + FixB = FALSE + FixC = FALSE + FixD = FALSE + PlantBug = FALSE +SPECIFICATION Spec +INVARIANT TypeOK +INVARIANT WitnessCallerRuns +CHECK_DEADLOCK FALSE diff --git a/formal/binary-storage/tla/cfg/wit_orig_WitnessDone.cfg b/formal/binary-storage/tla/cfg/wit_orig_WitnessDone.cfg new file mode 100644 index 000000000..660cdec0e --- /dev/null +++ b/formal/binary-storage/tla/cfg/wit_orig_WitnessDone.cfg @@ -0,0 +1,18 @@ +CONSTANTS + Clusters <- ClustersR + Deps <- DepsR + NStore = 1 + QCap = 1 + MaxTimeouts = 1 + LoaderLoadsDeps = TRUE + AllowLoadFail = TRUE + AllowLinkFail = TRUE + FixA = FALSE + FixB = FALSE + FixC = FALSE + FixD = FALSE + PlantBug = FALSE +SPECIFICATION Spec +INVARIANT TypeOK +INVARIANT WitnessDone +CHECK_DEADLOCK FALSE diff --git a/formal/binary-storage/tla/cfg/wit_orig_WitnessGoodRead.cfg b/formal/binary-storage/tla/cfg/wit_orig_WitnessGoodRead.cfg new file mode 100644 index 000000000..526f22d81 --- /dev/null +++ b/formal/binary-storage/tla/cfg/wit_orig_WitnessGoodRead.cfg @@ -0,0 +1,18 @@ +CONSTANTS + Clusters <- ClustersR + Deps <- DepsR + NStore = 1 + QCap = 1 + MaxTimeouts = 1 + LoaderLoadsDeps = TRUE + AllowLoadFail = TRUE + AllowLinkFail = TRUE + FixA = FALSE + FixB = FALSE + FixC = FALSE + FixD = FALSE + PlantBug = FALSE +SPECIFICATION Spec +INVARIANT TypeOK +INVARIANT WitnessGoodRead +CHECK_DEADLOCK FALSE diff --git a/formal/binary-storage/tla/cfg/wit_orig_WitnessSecondClust.cfg b/formal/binary-storage/tla/cfg/wit_orig_WitnessSecondClust.cfg new file mode 100644 index 000000000..a00e0bd29 --- /dev/null +++ b/formal/binary-storage/tla/cfg/wit_orig_WitnessSecondClust.cfg @@ -0,0 +1,18 @@ +CONSTANTS + Clusters <- ClustersR + Deps <- DepsR + NStore = 1 + QCap = 1 + MaxTimeouts = 1 + LoaderLoadsDeps = TRUE + AllowLoadFail = TRUE + AllowLinkFail = TRUE + FixA = FALSE + FixB = FALSE + FixC = FALSE + FixD = FALSE + PlantBug = FALSE +SPECIFICATION Spec +INVARIANT TypeOK +INVARIANT WitnessSecondClust +CHECK_DEADLOCK FALSE diff --git a/formal/binary-storage/tla/cfg/wit_orig_WitnessStoreOk.cfg b/formal/binary-storage/tla/cfg/wit_orig_WitnessStoreOk.cfg new file mode 100644 index 000000000..c481515af --- /dev/null +++ b/formal/binary-storage/tla/cfg/wit_orig_WitnessStoreOk.cfg @@ -0,0 +1,18 @@ +CONSTANTS + Clusters <- ClustersR + Deps <- DepsR + NStore = 1 + QCap = 1 + MaxTimeouts = 1 + LoaderLoadsDeps = TRUE + AllowLoadFail = TRUE + AllowLinkFail = TRUE + FixA = FALSE + FixB = FALSE + FixC = FALSE + FixD = FALSE + PlantBug = FALSE +SPECIFICATION Spec +INVARIANT TypeOK +INVARIANT WitnessStoreOk +CHECK_DEADLOCK FALSE diff --git a/formal/binary-storage/tla/cfg/wit_orig_WitnessTimeout.cfg b/formal/binary-storage/tla/cfg/wit_orig_WitnessTimeout.cfg new file mode 100644 index 000000000..5966b6391 --- /dev/null +++ b/formal/binary-storage/tla/cfg/wit_orig_WitnessTimeout.cfg @@ -0,0 +1,18 @@ +CONSTANTS + Clusters <- ClustersR + Deps <- DepsR + NStore = 1 + QCap = 1 + MaxTimeouts = 1 + LoaderLoadsDeps = TRUE + AllowLoadFail = TRUE + AllowLinkFail = TRUE + FixA = FALSE + FixB = FALSE + FixC = FALSE + FixD = FALSE + PlantBug = FALSE +SPECIFICATION Spec +INVARIANT TypeOK +INVARIANT WitnessTimeout +CHECK_DEADLOCK FALSE diff --git a/formal/binary-storage/tla/check_all.sh b/formal/binary-storage/tla/check_all.sh new file mode 100755 index 000000000..3c37236a5 --- /dev/null +++ b/formal/binary-storage/tla/check_all.sh @@ -0,0 +1,41 @@ +#!/bin/sh +# Regenerates every configuration and runs TLC on it; prints one summary line per run. +# Runs taking a minute or more only run with FULL=1 (orig_live_M alone is ~9 min). +cd "$(dirname "$0")" +SAFE="TypeOK NotSourceOnlyWhenStored StoresAccounted LoaderNoPartialRead MainNoPartialRead NoStaleRead SetThreadSafe NoDetachedStore" +LIVE="BuildTerminates WorkersQuiesce StoreResolved" +WIT="WitnessDone WitnessSecondClust WitnessCallerRuns WitnessTimeout WitnessGoodRead WitnessStoreOk" +run() { # name size nstore qcap maxto ldeps lfail linkfail fixA fixB fixC fixD plant "inv" "props" + n=$1; shift + ./gen.sh "$n" "$@" + out=$(./run.sh "cfg/$n.cfg" 2>&1) + res=$(echo "$out" | grep -E "^Error: (Invariant|Temporal|Deadlock)|is violated" | head -1) + [ -z "$res" ] && res=$(echo "$out" | grep -q "No error has been found" && echo "OK" || echo "$out" | grep -E "Error" | head -1) + st=$(echo "$out" | grep -E "distinct states found" | tail -1 | sed -E 's/.* ([0-9]+) distinct states found.*/\1/') + t=$(echo "$out" | grep -E "^Finished in" | sed -E 's/Finished in ([^ ]+).*/\1/') + printf '%-28s %-58s %8s distinct %s\n' "$n" "$res" "$st" "$t" +} +# --- the code as written (all environment behaviours on) ----------------------------------------- +for p in $SAFE; do run "orig_$p" S 1 1 1 TRUE TRUE TRUE FALSE FALSE FALSE FALSE FALSE "$p" ""; done +run orig_live S 1 1 1 TRUE TRUE TRUE FALSE FALSE FALSE FALSE FALSE "" "$LIVE" +[ -n "${FULL:-}" ] && run orig_live_M M 1 1 1 TRUE FALSE FALSE FALSE FALSE FALSE FALSE FALSE "" "$LIVE" +# happy environment: no timeouts, no failures, loaders do not load dependencies +for p in NotSourceOnlyWhenStored LoaderNoPartialRead MainNoPartialRead NoStaleRead SetThreadSafe NoDetachedStore; do + run "happy_$p" M 2 1 0 FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE "$p" ""; done +# --- fixed model: FixA..FixD, every environment behaviour on, growing sizes ---------------------- +run fixed_S S 1 1 1 TRUE TRUE TRUE TRUE TRUE TRUE TRUE FALSE "$SAFE" "$LIVE" +run fixed_M M 1 1 1 TRUE TRUE TRUE TRUE TRUE TRUE TRUE FALSE "$SAFE" "$LIVE" +[ -n "${FULL:-}" ] && run fixed_M2 M 2 1 1 TRUE TRUE TRUE TRUE TRUE TRUE TRUE FALSE "$SAFE" "$LIVE" +[ -n "${FULL:-}" ] && run fixed_L L 1 1 1 TRUE TRUE TRUE TRUE TRUE TRUE TRUE FALSE "$SAFE" "$LIVE" +run fixed_L2 L 2 1 2 TRUE TRUE TRUE TRUE TRUE TRUE TRUE FALSE "$SAFE" "" +[ -n "${FULL:-}" ] && run fixed_R R 1 1 1 TRUE TRUE TRUE TRUE TRUE TRUE TRUE FALSE "$SAFE" "$LIVE" +# --- ablations: fixed model with one fix undone ---------------------------------------------------- +run ablateA M 1 1 1 TRUE TRUE TRUE FALSE TRUE TRUE TRUE FALSE "$SAFE" "" +run ablateB M 1 1 1 TRUE TRUE TRUE TRUE FALSE TRUE TRUE FALSE "$SAFE" "" +run ablateC M 1 1 1 TRUE TRUE TRUE TRUE TRUE FALSE TRUE FALSE "$SAFE" "" +run ablateD M 1 1 1 TRUE TRUE TRUE TRUE TRUE TRUE FALSE FALSE "$SAFE" "" +# --- planted bug in the fixed model ------------------------------------------------------------------ +run planted S 1 1 1 TRUE TRUE TRUE TRUE TRUE TRUE TRUE TRUE "$SAFE" "" +# --- witnesses (each must be violated) ------------------------------------------------------------- +for w in $WIT; do run "wit_orig_$w" R 1 1 1 TRUE TRUE TRUE FALSE FALSE FALSE FALSE FALSE "$w" ""; done +for w in $WIT; do run "wit_fixed_$w" R 1 1 1 TRUE TRUE TRUE TRUE TRUE TRUE TRUE FALSE "$w" ""; done diff --git a/formal/binary-storage/tla/expected.txt b/formal/binary-storage/tla/expected.txt new file mode 100644 index 000000000..cb325c1e9 --- /dev/null +++ b/formal/binary-storage/tla/expected.txt @@ -0,0 +1,39 @@ +orig_TypeOK OK +orig_NotSourceOnlyWhenStored VIOLATED:NotSourceOnlyWhenStored +orig_StoresAccounted OK +orig_LoaderNoPartialRead VIOLATED:LoaderNoPartialRead +orig_MainNoPartialRead VIOLATED:MainNoPartialRead +orig_NoStaleRead VIOLATED:NoStaleRead +orig_SetThreadSafe VIOLATED:SetThreadSafe +orig_NoDetachedStore VIOLATED:NoDetachedStore +orig_live OK +orig_live_M OK [full] +happy_NotSourceOnlyWhenStored VIOLATED:NotSourceOnlyWhenStored +happy_LoaderNoPartialRead OK +happy_MainNoPartialRead OK +happy_NoStaleRead OK +happy_SetThreadSafe VIOLATED:SetThreadSafe +happy_NoDetachedStore OK +fixed_S OK +fixed_M OK +fixed_M2 OK [full] +fixed_L OK [full] +fixed_L2 OK +fixed_R OK [full] +ablateA VIOLATED:NotSourceOnlyWhenStored +ablateB VIOLATED:SetThreadSafe +ablateC VIOLATED:NoDetachedStore +ablateD VIOLATED:NoDetachedStore +planted VIOLATED:NotSourceOnlyWhenStored +wit_orig_WitnessDone VIOLATED:WitnessDone +wit_orig_WitnessSecondClust VIOLATED:WitnessSecondClust +wit_orig_WitnessCallerRuns VIOLATED:WitnessCallerRuns +wit_orig_WitnessTimeout VIOLATED:WitnessTimeout +wit_orig_WitnessGoodRead VIOLATED:WitnessGoodRead +wit_orig_WitnessStoreOk VIOLATED:WitnessStoreOk +wit_fixed_WitnessDone VIOLATED:WitnessDone +wit_fixed_WitnessSecondClust VIOLATED:WitnessSecondClust +wit_fixed_WitnessCallerRuns VIOLATED:WitnessCallerRuns +wit_fixed_WitnessTimeout VIOLATED:WitnessTimeout +wit_fixed_WitnessGoodRead VIOLATED:WitnessGoodRead +wit_fixed_WitnessStoreOk VIOLATED:WitnessStoreOk diff --git a/formal/binary-storage/tla/gen.sh b/formal/binary-storage/tla/gen.sh new file mode 100755 index 000000000..f5980e5e0 --- /dev/null +++ b/formal/binary-storage/tla/gen.sh @@ -0,0 +1,25 @@ +#!/bin/sh +# usage: gen.sh NAME SIZE(S|M|L) NSTORE QCAP MAXTO LDEPS LFAIL LINKFAIL FIXA FIXB FIXC FIXD PLANT "INVARIANTS" "PROPERTIES" +cd "$(dirname "$0")"; mkdir -p cfg +n=$1; sz=$2 +cat > cfg/$n.cfg <> cfg/$n.cfg; done +for p in ${15}; do echo "PROPERTY $p" >> cfg/$n.cfg; done +echo "CHECK_DEADLOCK FALSE" >> cfg/$n.cfg diff --git a/formal/binary-storage/tla/run.sh b/formal/binary-storage/tla/run.sh new file mode 100755 index 000000000..28d7e70a5 --- /dev/null +++ b/formal/binary-storage/tla/run.sh @@ -0,0 +1,6 @@ +#!/bin/sh +# usage: ./run.sh cfg/X.cfg [extra TLC args] (checks MC.tla, i.e. BinaryStorage with the size definitions) +cd "$(dirname "$0")" +cfg=$1; shift +exec java -XX:+UseParallelGC -cp ../../.tools/tla2tools.jar tlc2.TLC -workers auto \ + -metadir "states/$(basename "$cfg" .cfg)" -config "$cfg" "$@" MC.tla diff --git a/formal/binary-storage/tla/trace.py b/formal/binary-storage/tla/trace.py new file mode 100755 index 000000000..0fdd972c1 --- /dev/null +++ b/formal/binary-storage/tla/trace.py @@ -0,0 +1,29 @@ +#!/usr/bin/env python3 +"""Condense a TLC counterexample: print each step's action and only the variables that changed.""" +import re, sys +txt = sys.stdin.read() +m = re.search(r"Error: (.*?)\n", txt) +if m: print("ERROR:", m.group(1)) +states = re.split(r"\nState (\d+): ", txt) +prev = {} +for i in range(1, len(states), 2): + n, body = states[i], states[i + 1] + body = body.split("\n\n")[0] + head, _, rest = body.partition("\n") + act = re.match(r"<(\w+)", head) + act = act.group(1) if act else head.strip() + cur = {} + for vm in re.finditer(r"^/\\ (\w+) = (.*?)(?=^/\\ |\Z)", rest, re.S | re.M): + cur[vm.group(1)] = " ".join(vm.group(2).split()) + diff = {k: v for k, v in cur.items() if prev.get(k) != v} + if n == "1": + keep = ("binary", "sources", "queue", "lpc") + diff = {k: v for k, v in cur.items() if k in keep} + print(f"{n:>3} {act:<11} " + "; ".join(f"{k}={v}" for k, v in sorted(diff.items()))) + prev = cur + if "Back to state" in body or "Stuttering" in body: + print(" ", [l for l in body.splitlines() if "Back to state" in l or "Stuttering" in l]) +m = re.search(r"(\d+) states generated, (\d+) distinct states found", txt) +if m: print("states:", m.group(1), "generated,", m.group(2), "distinct") +m = re.search(r"depth of the complete state graph search is (\d+)", txt) +if m: print("depth:", m.group(1)) diff --git a/formal/check.sh b/formal/check.sh new file mode 100755 index 000000000..2a10bb025 --- /dev/null +++ b/formal/check.sh @@ -0,0 +1,182 @@ +#!/usr/bin/env bash +# Local validation harness for formal/: TLC matrices vs golden verdicts, Lean builds and axioms, orphan-test check. +# Usage: formal/check.sh [--clean] [--full] [--update] [--only=|orphans] +# --clean delete .lake/, states/ and TLC metadirs first +# --full also run the expensive TLC runs (tagged [full] in expected.txt) +# --update rewrite expected.txt / theorems.txt / orphans expected.txt from this run (review the diff!) +set -u +F="$(cd "$(dirname "$0")" && pwd)" +TARGETS="parallel-loader binary-storage find-refs trie pipeline" +JAR="$F/.tools/tla2tools.jar" +JAR_SHA=936a262061c914694dfd669a543be24573c45d5aa0ff20a8b96b23d01e050e88 +LEAN_TC=leanprover/lean4:v4.35.0-rc2 +OUT="$F/.check" +FULL= CLEAN= UPDATE= ONLY= +for a in "$@"; do + case $a in + --full) FULL=1 ;; --clean) CLEAN=1 ;; --update) UPDATE=1 ;; --only=*) ONLY=${a#--only=} ;; + -h|--help) sed -n '2,7p' "$0" | sed 's/^# \{0,1\}//'; exit 0 ;; + *) echo "unknown argument: $a" >&2; exit 2 ;; + esac +done +case " $TARGETS orphans " in *" ${ONLY:-orphans} "*) ;; *) echo "unknown target: $ONLY" >&2; exit 2 ;; esac +[ -n "$ONLY" ] && TARGETS=${ONLY#orphans} +export FULL + +if [ -n "$CLEAN" ]; then + echo "cleaning .lake/, states/, TLC metadirs" + find "$F" -type d \( -name .lake -o -name states -o -name 'meta-*' \) -prune -exec rm -rf {} + + rm -rf "$F/find-refs/tla/meta" "$OUT" +fi +mkdir -p "$OUT" +T0=$(date +%s) +SUMMARY="$OUT/summary.txt"; : > "$SUMMARY" +result() { printf '%-28s %-4s %s\n' "$1" "$2" "$3" >> "$SUMMARY"; } + +# ---------------------------------------------------------------- TLA+ +# Maps a TLC log (stdin) to OK | VIOLATED: | DEADLOCK | ERROR; temporal violations are unnamed by TLC. +VERDICT=' +function verdict(s) { + if (match(s, /Invariant [A-Za-z0-9_]+ is violated/)) return "VIOLATED:" substr(s, RSTART + 10, RLENGTH - 22) + if (match(s, /Evaluating invariant [A-Za-z0-9_]+ failed/)) return "VIOLATED:" substr(s, RSTART + 21, RLENGTH - 28) + if (s ~ /Temporal properties were violated/) return "VIOLATED:TEMPORAL" + if (s ~ /Deadlock reached/) return "DEADLOCK" + if (s ~ /No error has been found/) return "OK" + return "ERROR" +}' +classify() { # name logfile + if [ -f "$2" ]; then awk -v n="$1" "$VERDICT"' { b = b $0 "\n" } END { print n, verdict(b) }' "$2"; else echo "$1 ERROR"; fi +} + +tla_matrix() { # target -> normalised " " lines on stdout + local d="$F/$1/tla" + case $1 in + parallel-loader) sh "$d/check_all.sh" | awk "$VERDICT"' NF { print $1 ":" $2, verdict($0) }' ;; + binary-storage) sh "$d/check_all.sh" | awk "$VERDICT"' NF { print $1, ($2 == "OK" ? "OK" : verdict($0)) }' ;; + find-refs) bash "$d/matrix.sh" | sed -n 's/^== \([^ ]*\) .*/\1/p' | while read -r n; do classify "$n" "$d/runs/$n.out"; done ;; + trie) sh "$d/runall.sh" | awk '{ print $2 }' | while read -r n; do classify "$n" "$d/out/$n.log"; done ;; + pipeline) bash "$d/run_all.sh" ${FULL:+--live} | awk '{ print $1 }' | while read -r n; do classify "$n" "$d/logs/$n.log"; done ;; + esac +} + +tla_ok=1 +if ! command -v java >/dev/null; then + echo "java not found"; tla_ok= +elif [ ! -f "$JAR" ]; then + echo "missing $JAR; fetch it with:" + echo " gh release download v1.7.4 -R tlaplus/tlaplus -p tla2tools.jar -D formal/.tools" + echo " expected SHA-256 $JAR_SHA"; tla_ok= +else + sha=$( (shasum -a 256 "$JAR" 2>/dev/null || sha256sum "$JAR") | cut -d' ' -f1) + [ "$sha" = "$JAR_SHA" ] || { echo "tla2tools.jar SHA-256 mismatch: $sha (expected $JAR_SHA)"; tla_ok=; } +fi + +tla_check() { # target + local t=$1 gold="$F/$1/tla/expected.txt" got="$OUT/$1.tla.txt" s=$(date +%s) + [ -n "$tla_ok" ] || { result "$t/tla" FAIL "TLC unavailable"; return; } + echo "== $t/tla" + tla_matrix "$t" > "$got" + if [ -n "$UPDATE" ]; then + # keep the [full] tags of runs that were skipped this time + awk 'NR == FNR { seen[$1] = 1; print; next } $3 == "[full]" && !($1 in seen)' "$got" "$gold" 2>/dev/null > "$got.new" + [ -n "$FULL" ] && [ -f "$gold" ] && awk 'NR == FNR { if ($3 == "[full]") full[$1] = 1; next } { print $0 (($1 in full) ? " [full]" : "") }' "$gold" "$got.new" > "$got.tag" && mv "$got.tag" "$got.new" + mv "$got.new" "$gold" + fi + local want="$OUT/$t.tla.want" + if [ -n "$FULL" ]; then awk 'NF && $1 !~ /^#/ { print $1, $2 }' "$gold"; else awk 'NF && $1 !~ /^#/ && $3 != "[full]" { print $1, $2 }' "$gold"; fi 2>/dev/null | sort > "$want" + if diff <(sort "$got") "$want" > "$OUT/$t.tla.diff"; then + result "$t/tla" PASS "$(wc -l < "$got" | tr -d ' ') runs, $(( $(date +%s) - s ))s" + else + sed 's/^/ /' "$OUT/$t.tla.diff" + result "$t/tla" FAIL "golden mismatch (< got, > expected), $(( $(date +%s) - s ))s" + fi +} + +# ---------------------------------------------------------------- Lean +# Lists every user-written theorem of the package (declaration ranges exclude generated lemmas). +lean_probe() { # libs... -> Lean source on stdout + echo "import Lean.Elab.Command" + for l in "$@"; do echo "import $l"; done + printf 'open Lean in\nrun_cmd do\n let env ← getEnv\n let roots : List Name := [%s]\n' "$(printf '`%s, ' "$@" | sed 's/, $//')" + cat <<'EOF' + for (n, ci) in env.constants.map₁.toList do + if let .thmInfo _ := ci then + unless n.isInternal do + if let some idx := env.getModuleIdxFor? n then + if roots.contains env.header.moduleNames[idx.toNat]!.getRoot then + if (← findDeclarationRanges? n).isSome then IO.println s!"THM {n}" +EOF +} + +lean_check() { # target; prints details to stdout, one summary via result() + local t=$1 d="$F/$1/lean" log="$OUT/$1.lean.log" s=$(date +%s) fail= + local tc; tc=$(tr -d '[:space:]' < "$d/lean-toolchain") + [ "$tc" = "$LEAN_TC" ] || { result "$t/lean" FAIL "toolchain $tc, want $LEAN_TC"; return; } + elan toolchain list 2>/dev/null | grep -q "^$tc" || { result "$t/lean" FAIL "$tc not installed (no downloads)"; return; } + (cd "$d" && lake build) > "$log" 2>&1 || { tail -20 "$log"; result "$t/lean" FAIL "lake build failed ($log)"; return; } + # sorry/admit outside comments, or reported by the elaborator + local holes; holes=$(fd -0 -e lean -E .lake . "$d" | xargs -0 perl -0777 -ne 's{/-.*?-/}{}gs; s{--[^\n]*}{}g; print "$ARGV\n" if /\b(sorry|admit)\b/') + grep -q "declaration uses 'sorry'" "$log" && holes="$holes (build log)" + [ -n "$holes" ] && { echo "sorry/admit in: $holes"; fail=1; } + local libs; libs=$(awk '/^\[/ { sec = $0 } sec == "[[lean_lib]]" && /^name *=/ { gsub(/^name *= *"|"$/, ""); print }' "$d/lakefile.toml") + local list="$d/theorems.txt" probe="$d/.lake/check_axioms.lean" pout="$OUT/$t.axioms.txt" + lean_probe $libs > "$probe" + (cd "$d" && lake env lean "$probe") 2>&1 | awk '/^THM / { print $2 }' | sort > "$OUT/$t.all" + # #print axioms for every listed and every declared theorem + { lean_probe $libs; { [ -f "$list" ] && awk 'NF && $1 !~ /^#/ { print $1 }' "$list"; cat "$OUT/$t.all"; } | sort -u | sed 's/^/#print axioms /'; } > "$probe" + (cd "$d" && lake env lean "$probe") > "$pout" 2>&1 + # one line per theorem: + awk ' + function flush() { if (n == "") return + k = "kernel"; split(ax, a, /[][, ]+/) + for (i in a) if (a[i] != "" && a[i] !~ /^(propext|Classical\.choice|Quot\.sound)$/) { + if (a[i] ~ /^(Lean\.ofReduceBool|Lean\.trustCompiler)$/ || a[i] ~ /\._native\.native_decide\.ax_[0-9_]+$/) { if (k == "kernel") k = "native_decide" } + else { k = "BAD:" a[i]; break } } + print n, k; n = "" } + /^THM / { next } + /^'\''/ { flush(); n = $0; sub(/^'\''/, "", n); sub(/'\''.*/, "", n); ax = $0; sub(/^[^:]*:/, "", ax) + if ($0 ~ /does not depend on any axioms/) ax = ""; next } + n != "" { ax = ax " " $0 } + END { flush() }' "$pout" | sort > "$OUT/$t.got" + [ -n "$UPDATE" ] && { echo "# ; checked by formal/check.sh via #print axioms"; cat "$OUT/$t.got"; } > "$list" + grep -Eq ':[0-9]+:[0-9]+: error' "$pout" && { grep -E ': error' "$pout" | head -5; fail=1; } + awk 'NF && $1 !~ /^#/ { print $1, $2 }' "$list" | sort > "$OUT/$t.want" + if ! diff <(awk '{ print $1 }' "$OUT/$t.want") "$OUT/$t.all" > /dev/null; then + echo "theorem list drift (< theorems.txt, > declared):"; diff <(awk '{ print $1 }' "$OUT/$t.want") "$OUT/$t.all" | grep '^[<>]'; fail=1 + fi + if ! diff "$OUT/$t.got" "$OUT/$t.want" > "$OUT/$t.lean.diff"; then + echo "axiom class mismatch (< actual, > theorems.txt):"; grep '^[<>]' "$OUT/$t.lean.diff"; fail=1 + fi + awk '{ printf " %-66s %s\n", $1, $2 }' "$OUT/$t.got" + local nk nn; nk=$(grep -c ' kernel$' "$OUT/$t.got"); nn=$(grep -c ' native_decide$' "$OUT/$t.got") + result "$t/lean" "$([ -n "$fail" ] && echo FAIL || echo PASS)" "$nk kernel + $nn native_decide theorems, $(( $(date +%s) - s ))s" +} + +# ---------------------------------------------------------------- orphaned tests +orphans_check() { # runs on a snapshot of HEAD so uncommitted work in the tree does not change the verdict + local o="$F/readonly/orphans" snap got="$OUT/orphans.txt" s=$(date +%s) + snap=$(mktemp -d "${TMPDIR:-/tmp}/formal-check.XXXXXX") + git -C "$(git -C "$F" rev-parse --show-toplevel)" archive HEAD | tar -x -C "$snap" + "$o/check-test-reachability.sh" "$snap" > "$OUT/orphans.log" 2>&1; local rc=$? + rm -rf "$snap" + { echo "exit $rc"; awk -F'\t' '$1 ~ /UNREACHABLE$/ { print "UNREACHABLE", $3 }' "$OUT/orphans.log" | sort; } > "$got" + "$o/selftest.sh" > "$OUT/orphans-selftest.log" 2>&1 && echo "selftest exit 0" >> "$got" || echo "selftest exit $?" >> "$got" + [ -n "$UPDATE" ] && cp "$got" "$o/expected.txt" + if diff "$got" "$o/expected.txt" > "$OUT/orphans.diff"; then + result readonly/orphans PASS "exit $rc as expected, $(grep -c ^UNREACHABLE "$got") unreachable, $(( $(date +%s) - s ))s" + else + sed 's/^/ /' "$OUT/orphans.diff"; result readonly/orphans FAIL "outcome differs from expected.txt" + fi +} + +# Lean builds run in the background while TLC runs in the foreground. +( for t in $TARGETS; do lean_check "$t" > "$OUT/$t.lean.report" 2>&1; done ) & +LEAN_PID=$! +for t in $TARGETS; do tla_check "$t"; done +[ -z "$ONLY" ] || [ "$ONLY" = orphans ] && orphans_check +wait $LEAN_PID +for t in $TARGETS; do echo "== $t/lean"; cat "$OUT/$t.lean.report"; done + +echo; echo "== summary ($(( $(date +%s) - T0 ))s${FULL:+, --full})" +sort "$SUMMARY" +! grep -q ' FAIL ' "$SUMMARY" diff --git a/formal/find-refs/lean/.gitignore b/formal/find-refs/lean/.gitignore new file mode 100644 index 000000000..01f8cdb63 --- /dev/null +++ b/formal/find-refs/lean/.gitignore @@ -0,0 +1 @@ +.lake/ diff --git a/formal/find-refs/lean/FindRefs.lean b/formal/find-refs/lean/FindRefs.lean new file mode 100644 index 000000000..48fc04793 --- /dev/null +++ b/formal/find-refs/lean/FindRefs.lean @@ -0,0 +1,6 @@ +import FindRefs.State +import FindRefs.Buggy +import FindRefs.Fixed +import FindRefs.Check +import FindRefs.Proof +import FindRefs.Theorems diff --git a/formal/find-refs/lean/FindRefs/Buggy.lean b/formal/find-refs/lean/FindRefs/Buggy.lean new file mode 100644 index 000000000..d8801514c --- /dev/null +++ b/formal/find-refs/lean/FindRefs/Buggy.lean @@ -0,0 +1,127 @@ +/- +Faithful model of FastReferenceSearchResultContentProvider as written (FRS = that file). +Every shared-memory access that is not protected by a common lock is its own step. +-/ +import FindRefs.State + +namespace FindRefs.Buggy +open FindRefs + +/-- Individual repairs, applied one at a time to expose bugs masked by earlier ones. + `Patch.none` is the code as written. -/ +structure Patch where + lost : Bool := false -- batch-add/flag test-and-set and isEmpty/flag-clear under the batch lock + order : Bool := false -- inputChanged: removeListener(old) before rootNodes.clear() + snap : Bool := false -- inputChanged: iterate a snapshot copy of matchingReferences + async : Bool := false -- Reset via asyncExec instead of syncExec (does not wait) +deriving Repr + +def Patch.none : Patch := {} + +/-- Search-thread steps. -/ +def sStep (P : Patch) (c : Cfg) (s : St) : List (String × St) := + match s.spc with + | .idle => searchStarts c s + | .fire r => + -- RSR.fireEvent: synchronized(listeners) { for l : listeners ... } + if s.listening then [(s!"S RSR.fireEvent(Added ref{r}) takes listeners lock -> FRS:170", { s with lockS := true, spc := .get r })] + else [(s!"S RSR.fireEvent(Added ref{r}): FRS not a listener, dropped", { s with spc := .idle })] + | .get r => + let u := uriOfRef s r + match getRoot s.roots u with + | some n => [(s!"S FRS:158 rootNodes.get(uri{u}) = node{n}", { s with spc := .child r n })] + | none => [(s!"S FRS:158 rootNodes.get(uri{u}) = null", { s with spc := .put r })] + | .put r => + let u := uriOfRef s r + let n := s.nodes.length + [(s!"S FRS:160-161 rootNodes.put(uri{u}, node{n})", + { s with nodes := s.nodes ++ [(u, epochOfRef s r)], roots := setRoot s.roots u (some n), spc := .bat r n })] + | .bat r n => [(s!"S FRS:162-164 batchAddNodes.add(node{n})", { s with batch := s.batch ++ [n], spc := .child r n })] + | .child r n => [(s!"S FRS:137 attach ref{r} under node{n}", { s with attach := s.attach ++ [(r, n)], spc := .flg })] + | .flg => + if P.lost then + if s.flag then [("S [patched] synchronized(batch){flag already true}; release listeners lock", { s with spc := .idle, lockS := false })] + else [("S [patched] synchronized(batch){flag := true; schedule}; release listeners lock", { s with flag := true, jobs := s.jobs + 1, spc := .idle, lockS := false })] + else if s.flag then [("S FRS:173 isUIUpdateScheduled == true -> skip schedule; release listeners lock", { s with spc := .idle, lockS := false })] + else [("S FRS:173 isUIUpdateScheduled == false", { s with spc := .setf })] + | .setf => [("S FRS:174 isUIUpdateScheduled = true", { s with flag := true, spc := .sched })] + | .sched => [("S FRS:175 new UIUpdater().schedule(); release listeners lock", { s with jobs := s.jobs + 1, spc := .idle, lockS := false })] + | .rfire => + if s.listening then + if P.async then [("S [patched] RSR.fireEvent(Reset) -> Display.asyncExec (no wait)", { s with syncReq := true, spc := .idle })] + else [("S RSR.fireEvent(Reset) takes listeners lock -> FRS:178 Display.syncExec (blocks)", { s with lockS := true, syncReq := true, spc := .rwait })] + else [("S RSR.fireEvent(Reset): FRS not a listener, dropped", { s with spc := .idle, resetPending := false })] + | .rwait => + if s.syncReq then [] else [("S FRS:178 syncExec returns; release listeners lock", { s with lockS := false, spc := .idle })] + +/-- UI-thread steps. -/ +def uStep (P : Patch) (_c : Cfg) (s : St) : List (String × St) := + match s.upc with + | .idle => + (if s.jobs > 0 then + [(s!"UI UIUpdater starts: FRS:207-210 snapshot+clear batch {s.batch}; FRS:212-215 viewer.add each", + { s with jobs := s.jobs - 1, batch := [], viewer := s.batch.foldr sins s.viewer, upc := .uRefresh })] + else []) ++ + (if s.syncReq then + [("UI Reset runnable FRS:181-186: viewer.remove(rootNodes.values), rootNodes.clear, refresh", + { s with roots := clearRoots s.roots, viewer := [], syncReq := false, resetPending := false })] + else []) ++ + (if s.switchB > 0 && s.input == .A then + if P.order then + [("UI [patched] user shows other result B: inputChanged(A,B) removeListener first", + { s with switchB := s.switchB - 1, upc := .wRemove })] + else + [("UI user shows other result B: setInput(B) -> inputChanged(A,B) FRS:111 rootNodes.clear", + { s with switchB := s.switchB - 1, roots := clearRoots s.roots, upc := .wRemove })] + else []) ++ + (if s.switchB > 0 && s.input == .B then + [("UI user shows result A again: setInput(A) -> inputChanged(B,A) FRS:111 rootNodes.clear", + { s with switchB := s.switchB - 1, roots := clearRoots s.roots, upc := .bAdd })] + else []) + | .uRefresh => [("UI FRS:216 viewer.refresh() (root items := rootNodes.values)", { s with viewer := sset (rootsVals s.roots), upc := .uCheck })] + | .uCheck => + if P.lost then + if s.batch.isEmpty then [("UI [patched] synchronized(batch){empty -> flag := false}", { s with flag := false, upc := .idle })] + else [("UI [patched] synchronized(batch){non-empty -> schedule(250)}", { s with jobs := s.jobs + 1, upc := .idle })] + else [(s!"UI FRS:217 batchAddNodes.isEmpty() = {s.batch.isEmpty}", { s with upc := .uDecide s.batch.isEmpty })] + | .uDecide e => + if e then [("UI FRS:220 isUIUpdateScheduled = false", { s with flag := false, upc := .idle })] + else [("UI FRS:218 schedule(250)", { s with jobs := s.jobs + 1, upc := .idle })] + | .wRemove => + -- RSR.removeListener is synchronized(listeners): blocks while S holds it + if s.lockS then [] + else if P.order then [("UI [patched] A.removeListener(this); rootNodes.clear", { s with listening := false, roots := clearRoots s.roots, upc := .wFinish })] + else [("UI FRS:113 A.removeListener(this)", { s with listening := false, upc := .wFinish })] + | .wFinish => [("UI FRS:116 B.addListener; ContentViewer.setInput(B) refresh", { s with input := .B, viewer := sset (rootsVals s.roots), upc := .idle })] + | .bAdd => + if s.lockS then [] + else [("UI FRS:116 A.addListener(this)", { s with listening := true, upc := .bIter })] + | .bIter => + if P.snap then [("UI [patched] snapshot = copy of matchingReferences", { s with snap := some s.matching, upc := .bLoop 0 s.mc })] + else [("UI FRS:118 matchingReferences.iterator()", { s with upc := .bLoop 0 s.mc })] + | .bLoop cur m => + let l := s.snap.getD s.matching + if cur == l.length then [("UI FRS:118 iterator.hasNext() = false", { s with snap := none, upc := .bDone })] + else if s.snap.isNone && s.mc != m then [("UI FRS:118 iterator.next() throws ConcurrentModificationException", { s with cme := true, upc := .idle })] + else + let r := (l[cur]?).getD 0 + [(s!"UI FRS:118 next() = ref{r}", { s with upc := .bGet cur m r })] + | .bGet cur m r => + let u := uriOfRef s r + match getRoot s.roots u with + | some n => [(s!"UI FRS:119->158 rootNodes.get(uri{u}) = node{n}", { s with upc := .bChild cur m r n })] + | none => [(s!"UI FRS:119->158 rootNodes.get(uri{u}) = null", { s with upc := .bPut cur m r })] + | .bPut cur m r => + let u := uriOfRef s r + let n := s.nodes.length + [(s!"UI FRS:119->160-161 rootNodes.put(uri{u}, node{n})", + { s with nodes := s.nodes ++ [(u, epochOfRef s r)], roots := setRoot s.roots u (some n), upc := .bBat cur m r n })] + | .bBat cur m r n => [(s!"UI FRS:119->162-164 batchAddNodes.add(node{n})", { s with batch := s.batch ++ [n], upc := .bChild cur m r n })] + | .bChild cur m r n => [(s!"UI FRS:119->137 attach ref{r} under node{n}", { s with attach := s.attach ++ [(r, n)], upc := .bLoop (cur + 1) m })] + | .bDone => [("UI ContentViewer.setInput(A): input := A; refresh", { s with input := .A, viewer := sset (rootsVals s.roots), resetPending := s.resetPending && resetInFlight s, upc := .idle })] + | .uDecideF | .wFix | .bFix => [] + +def next (P : Patch) (c : Cfg) (s : St) : List (String × St) := + if s.cme then [] else sStep P c s ++ uStep P c s + +end FindRefs.Buggy diff --git a/formal/find-refs/lean/FindRefs/Check.lean b/formal/find-refs/lean/FindRefs/Check.lean new file mode 100644 index 000000000..027767c4d --- /dev/null +++ b/formal/find-refs/lean/FindRefs/Check.lean @@ -0,0 +1,106 @@ +/- +Exhaustive BFS to a fixpoint, properties, and shortest-counterexample extraction. +-/ +import FindRefs.State + +namespace FindRefs +open Std + +abbrev Next := St → List (String × St) + +structure Explored where + order : Array St -- BFS discovery order + parent : HashMap St (Option (String × St)) -- predecessor + step label + edges : Nat + complete : Bool -- fixpoint reached within the cap + +/-- Breadth-first exploration until no new states (or `cap` states). -/ +def explore (next : Next) (init : St) (cap : Nat := 2000000) : Explored := Id.run do + let mut parent : HashMap St (Option (String × St)) := HashMap.emptyWithCapacity 4096 + parent := parent.insert init none + let mut order : Array St := #[init] + let mut i := 0 + let mut edges := 0 + -- `order` doubles as the BFS queue; loop bounded by `cap` + for _ in [0:cap] do + if h : i < order.size then + let s := order[i] + i := i + 1 + for (lbl, t) in next s do + edges := edges + 1 + if !parent.contains t then + parent := parent.insert t (some (lbl, s)) + order := order.push t + else + break + return { order, parent, edges, complete := i ≥ order.size } + +def trace (e : Explored) (s : St) : List String := Id.run do + let mut acc : List String := [] + let mut cur := s + for _ in [0:10000] do + match e.parent[cur]? with + | some (some (lbl, p)) => acc := lbl :: acc; cur := p + | _ => break + return acc + +/-! Properties -/ + +def uiIdle (s : St) : Bool := s.upc == .idle + +/-- No internal step pending: only environment actions (new accept/reset, user switches) remain. -/ +def quiescent (s : St) : Bool := + s.spc == .idle && s.upc == .idle && s.jobs == 0 && !s.syncReq && s.input == .A && s.listening && !s.cme + +/-- P1 no lost update: at quiescence every matching reference hangs under a shown root node. -/ +def p1 (s : St) : Bool := + !quiescent s || s.matching.all fun r => s.viewer.any fun n => s.attach.contains (r, n) + +/-- P1' (root-level form): at quiescence every current root node is shown. -/ +def p1root (s : St) : Bool := + !quiescent s || (rootsVals s.roots).all fun n => s.viewer.contains n + +/-- P2 one root node per URI: between UI runnables, no two shown root nodes share a URI. -/ +def p2 (s : St) : Bool := + !uiIdle s || (s.viewer.map (uriOfNode s)).Nodup + +/-- P3 no stale node: between UI runnables, once the viewer reflects the last reset, + every shown node belongs to the current input and the current search. -/ +def p3 (s : St) : Bool := + !uiIdle s || + (match s.input with + | .B => s.viewer.isEmpty + | .A => s.resetPending || s.viewer.all fun n => epochOfNode s n == s.epoch) + +/-- P4 no exception on the UI thread. -/ +def p4 (s : St) : Bool := !s.cme + +def props : List (String × (St → Bool)) := + [("P1 no lost update (refs)", p1), ("P1' no lost update (roots)", p1root), + ("P2 one root per URI", p2), ("P3 no stale node", p3), ("P4 no UI-thread CME", p4)] + +/-- Deadlock: no successor although some actor is still mid-flight. -/ +def deadlock (next : Next) (s : St) : Bool := + (next s).isEmpty && !s.cme && + !(s.spc == .idle && s.upc == .idle && s.jobs == 0 && !s.syncReq) + +def firstViolation (e : Explored) (p : St → Bool) : Option St := + e.order.find? fun s => !p s + +def allProps (next : Next) (e : Explored) : Bool := + e.complete && props.all (fun (_, p) => e.order.all p) && e.order.all (fun s => !deadlock next s) + +def report (name : String) (next : Next) (init : St) : IO Unit := do + let e := explore next init + IO.println s!"== {name}: {e.order.size} states, {e.edges} edges, fixpoint={e.complete}" + let checks := props ++ [("DL no deadlock", fun s => !deadlock next s)] + for (pn, p) in checks do + match firstViolation e p with + | none => IO.println s!" {pn}: holds" + | some s => + let t := trace e s + IO.println s!" {pn}: VIOLATED, shortest trace ({t.length} steps):" + for (l, k) in t.zipIdx do IO.println s!" {k+1}. {l}" + IO.println s!" final: roots={s.roots} batch={s.batch} flag={s.flag} jobs={s.jobs} viewer={s.viewer} matching={s.matching} attach={s.attach} nodes={s.nodes} epoch={s.epoch} input={repr s.input} spc={repr s.spc} upc={repr s.upc} lockS={s.lockS} syncReq={s.syncReq}" + +end FindRefs diff --git a/formal/find-refs/lean/FindRefs/Fixed.lean b/formal/find-refs/lean/FindRefs/Fixed.lean new file mode 100644 index 000000000..5f77bf2e8 --- /dev/null +++ b/formal/find-refs/lean/FindRefs/Fixed.lean @@ -0,0 +1,82 @@ +/- +Repaired design (not the Java as written). Changes w.r.t. FRS: + F1 addReference/resourceNode + flag test-and-set run atomically under one provider lock + (synchronized(batchAddNodes)); the UIUpdater's "batch empty? clear flag : reschedule" + is atomic under the same lock. [fixes lost update] + F2 Reset is handled on the search thread under that lock (clear rootNodes and batch, + ensure an updater is scheduled); no Display.syncExec, so no UI wait while the + RSR listeners monitor is held. [fixes deadlock, stale batch] + F3 inputChanged removes the old listener before clearing, and rebuilds from a + snapshot taken after addListener, under the provider lock; addReference skips a + reference already attached to the current root. [fixes stale-on-switch, CME, + duplicate root / lost ref] +`plant := true` plants an obvious bug (flag set without scheduling the job). +-/ +import FindRefs.State + +namespace FindRefs.Fixed +open FindRefs + +/-- resourceNode + attach child, deduplicated (part of the atomic addReference). -/ +def attachRef (s : St) (r : Nat) (withBatch : Bool) : St := + let u := uriOfRef s r + match getRoot s.roots u with + | some n => if s.attach.contains (r, n) then s else { s with attach := s.attach ++ [(r, n)] } + | none => + let n := s.nodes.length + { s with nodes := s.nodes ++ [(u, epochOfRef s r)], roots := setRoot s.roots u (some n), + batch := if withBatch then s.batch ++ [n] else s.batch, attach := s.attach ++ [(r, n)] } + +/-- Flag test-and-set under the batch lock. -/ +def ensureScheduled (plant : Bool) (s : St) : St := + if s.flag then s else { s with flag := true, jobs := if plant then s.jobs else s.jobs + 1 } + +/-- Atomic addReference under the provider lock (F1 + dedupe). -/ +def addRef (plant : Bool) (s : St) (r : Nat) : St := ensureScheduled plant (attachRef s r true) + +/-- Rebuild from a snapshot of matchingReferences (F3); the viewer is refreshed right after. -/ +def rebuild (s : St) : St := + s.matching.foldl (fun acc r => attachRef acc r false) { s with roots := clearRoots s.roots } + +def sStep (plant : Bool) (c : Cfg) (s : St) : List (String × St) := + match s.spc with + | .idle => searchStarts c s + | .fire r => + if s.listening then [(s!"S fireEvent(Added ref{r}) -> atomic addReference", { addRef plant s r with spc := .idle })] + else [(s!"S fireEvent(Added ref{r}): not a listener, dropped", { s with spc := .idle })] + | .rfire => + if s.listening then + [("S fireEvent(Reset) -> atomic clear rootNodes+batch, ensure updater", + ensureScheduled false { s with roots := clearRoots s.roots, batch := [], spc := .idle })] + else [("S fireEvent(Reset): not a listener, dropped", { s with spc := .idle, resetPending := false })] + | _ => [] + +def uStep (_c : Cfg) (s : St) : List (String × St) := + match s.upc with + | .idle => + (if s.jobs > 0 then + [("UI UIUpdater: atomic snapshot+clear batch, add, refresh", + { s with jobs := s.jobs - 1, batch := [], viewer := rootsVals s.roots, + resetPending := s.resetPending && resetInFlight s, upc := .uDecideF })] + else []) ++ + (if s.switchB > 0 && s.input == .A then + [("UI inputChanged(A,B): A.removeListener", { s with switchB := s.switchB - 1, listening := false, upc := .wFix })] + else []) ++ + (if s.switchB > 0 && s.input == .B then + [("UI inputChanged(B,A): A.addListener", { s with switchB := s.switchB - 1, listening := true, upc := .bFix })] + else []) + | .uDecideF => + if s.batch.isEmpty then [("UI atomic: batch empty -> flag := false", { s with flag := false, upc := .idle })] + else [("UI atomic: batch non-empty -> schedule(250)", { s with jobs := s.jobs + 1, upc := .idle })] + | .wFix => [("UI inputChanged(A,B): clear rootNodes+batch; setInput(B) refresh", + { s with roots := clearRoots s.roots, batch := [], input := .B, viewer := [], upc := .idle })] + | .bFix => [("UI inputChanged(B,A): rebuild from snapshot; setInput(A) refresh", + let s1 := rebuild s + { s1 with input := .A, viewer := rootsVals s1.roots, + resetPending := s.resetPending && resetInFlight s, upc := .idle })] + | _ => [] + +def next (plant : Bool) (c : Cfg) (s : St) : List (String × St) := + sStep plant c s ++ uStep c s + +end FindRefs.Fixed diff --git a/formal/find-refs/lean/FindRefs/Proof.lean b/formal/find-refs/lean/FindRefs/Proof.lean new file mode 100644 index 000000000..46190f01c --- /dev/null +++ b/formal/find-refs/lean/FindRefs/Proof.lean @@ -0,0 +1,203 @@ +/- +All-sizes proof (any Cfg: any number of URIs, accepts, resets, switches) for the fixed model: +"no lost root node": whenever no UIUpdater is scheduled or running, every root node in +rootNodes is shown in the viewer. Proved via an inductive invariant. +-/ +import FindRefs.Fixed + +namespace FindRefs.Proof +open FindRefs + +inductive Reach (next : St → List (String × St)) (init : St) : St → Prop + | init : Reach next init init + | step {s t : St} {l : String} : Reach next init s → (l, t) ∈ next s → Reach next init t + +def Inv (s : St) : Prop := + (s.batch ≠ [] → s.flag = true) ∧ + (s.flag = true → s.jobs > 0 ∨ s.upc = .uDecideF) ∧ + (∀ n ∈ rootsVals s.roots, n ∈ s.viewer ∨ n ∈ s.batch) + +theorem rootsVals_set (l : List (Option Nat)) (u n m : Nat) : + m ∈ rootsVals (setRoot l u (some n)) → m = n ∨ m ∈ rootsVals l := by + unfold rootsVals setRoot + simp only [List.mem_filterMap, id_eq, exists_eq_right] + intro h + rcases List.mem_or_eq_of_mem_set h with h | h + · exact Or.inr h + · exact Or.inl (Option.some.inj h) + +theorem rootsVals_clear (l : List (Option Nat)) : rootsVals (clearRoots l) = [] := by + unfold rootsVals clearRoots + induction l with + | nil => rfl + | cons x xs ih => simp + +theorem init_inv (c : Cfg) : Inv (St.init c) := by + refine ⟨?_, ?_, ?_⟩ + · simp [St.init] + · simp [St.init] + · intro n hn + have : rootsVals (List.replicate c.nU (none : Option Nat)) = [] := by + unfold rootsVals; induction c.nU <;> simp_all [List.replicate_succ] + simp [St.init, this] at hn + +/-- searchStarts only touches search-side fields. -/ +theorem searchStarts_frame (c : Cfg) (s : St) (p : String × St) (h : p ∈ searchStarts c s) : + p.2.batch = s.batch ∧ p.2.flag = s.flag ∧ p.2.jobs = s.jobs ∧ p.2.upc = s.upc ∧ + p.2.roots = s.roots ∧ p.2.viewer = s.viewer := by + unfold searchStarts at h + simp only [List.mem_append] at h + rcases h with h | h + · split at h + · simp only [List.mem_map, List.mem_range] at h + obtain ⟨_, _, rfl⟩ := h + simp + · simp at h + · split at h + · simp only [List.mem_cons, List.not_mem_nil, or_false] at h + subst h; simp + · simp at h + +theorem attachRef_frame (s : St) (r : Nat) (wb : Bool) : + (Fixed.attachRef s r wb).flag = s.flag ∧ (Fixed.attachRef s r wb).jobs = s.jobs ∧ + (Fixed.attachRef s r wb).upc = s.upc ∧ (Fixed.attachRef s r wb).viewer = s.viewer ∧ + (wb = false → (Fixed.attachRef s r wb).batch = s.batch) := by + unfold Fixed.attachRef + cases h : getRoot s.roots (uriOfRef s r) with + | none => cases wb <;> simp [h] + | some n => simp only [h]; split <;> simp + +theorem attachRef_cover (s : St) (r : Nat) + (h3 : ∀ n ∈ rootsVals s.roots, n ∈ s.viewer ∨ n ∈ s.batch) : + ∀ n ∈ rootsVals (Fixed.attachRef s r true).roots, + n ∈ (Fixed.attachRef s r true).viewer ∨ n ∈ (Fixed.attachRef s r true).batch := by + unfold Fixed.attachRef + cases h : getRoot s.roots (uriOfRef s r) with + | some n => simp only [h]; split <;> exact h3 + | none => + simp only [h, ite_true] + intro n hn + rcases rootsVals_set _ _ _ _ hn with h | h + · exact Or.inr (by simp [h]) + · rcases h3 n h with h' | h' + · exact Or.inl h' + · exact Or.inr (by simp [h']) + +theorem ensureScheduled_inv (s : St) + (h2 : s.flag = true → s.jobs > 0 ∨ s.upc = .uDecideF) + (h3 : ∀ n ∈ rootsVals s.roots, n ∈ s.viewer ∨ n ∈ s.batch) : + Inv (Fixed.ensureScheduled false s) := by + unfold Fixed.ensureScheduled + split + · rename_i hf; exact ⟨fun _ => hf, h2, h3⟩ + · exact ⟨fun _ => rfl, fun _ => Or.inl (by simp), h3⟩ + +theorem addRef_inv (s : St) (r : Nat) (hI : Inv s) : Inv (Fixed.addRef false s r) := by + obtain ⟨_, h2, h3⟩ := hI + obtain ⟨ef, ej, eu, _, _⟩ := attachRef_frame s r true + unfold Fixed.addRef + apply ensureScheduled_inv + · intro hf; rw [ej, eu]; exact h2 (ef ▸ hf) + · exact attachRef_cover s r h3 + +theorem rebuild_frame (s : St) : + (Fixed.rebuild s).batch = s.batch ∧ (Fixed.rebuild s).flag = s.flag ∧ + (Fixed.rebuild s).jobs = s.jobs ∧ (Fixed.rebuild s).upc = s.upc := by + unfold Fixed.rebuild + suffices ∀ (l : List Nat) (acc : St), acc.batch = s.batch → acc.flag = s.flag → acc.jobs = s.jobs → + acc.upc = s.upc → + let t := l.foldl (fun acc r => Fixed.attachRef acc r false) acc + t.batch = s.batch ∧ t.flag = s.flag ∧ t.jobs = s.jobs ∧ t.upc = s.upc from + this _ _ rfl rfl rfl rfl + intro l + induction l with + | nil => intro acc h1 h2 h3 h4; exact ⟨h1, h2, h3, h4⟩ + | cons r rs ih => + intro acc h1 h2 h3 h4 + obtain ⟨ef, ej, eu, _, eb⟩ := attachRef_frame acc r false + exact ih _ (by rw [eb rfl]; exact h1) (by rw [ef]; exact h2) (by rw [ej]; exact h3) (by rw [eu]; exact h4) + +theorem step_inv (c : Cfg) (s : St) (hI : Inv s) (p : String × St) (hp : p ∈ Fixed.next false c s) : + Inv p.2 := by + obtain ⟨h1, h2, h3⟩ := hI + unfold Fixed.next at hp + rcases List.mem_append.mp hp with hp | hp + · -- search thread + unfold Fixed.sStep at hp + split at hp + · obtain ⟨eb, ef, ej, eu, er, ev⟩ := searchStarts_frame c s p hp + exact ⟨by rw [eb, ef]; exact h1, by rw [ef, ej, eu]; exact h2, by rw [er, ev, eb]; exact h3⟩ + · split at hp + · simp only [List.mem_cons, List.not_mem_nil, or_false] at hp; subst hp + exact addRef_inv s _ ⟨h1, h2, h3⟩ + · simp only [List.mem_cons, List.not_mem_nil, or_false] at hp; subst hp + exact ⟨h1, h2, h3⟩ + · split at hp + · simp only [List.mem_cons, List.not_mem_nil, or_false] at hp; subst hp + apply ensureScheduled_inv + · exact h2 + · intro n hn; simp [rootsVals_clear] at hn + · simp only [List.mem_cons, List.not_mem_nil, or_false] at hp; subst hp + exact ⟨h1, h2, h3⟩ + · simp at hp + · -- UI thread + unfold Fixed.uStep at hp + split at hp + · simp only [List.mem_append] at hp + rcases hp with (hp | hp) | hp + · split at hp + · simp only [List.mem_cons, List.not_mem_nil, or_false] at hp; subst hp + refine ⟨fun h => absurd rfl h, fun _ => Or.inr rfl, fun n hn => Or.inl hn⟩ + · simp at hp + · split at hp + · simp only [List.mem_cons, List.not_mem_nil, or_false] at hp; subst hp + refine ⟨h1, fun hf => Or.inl ((h2 hf).resolve_right (by intro h; simp_all)), h3⟩ + · simp at hp + · split at hp + · simp only [List.mem_cons, List.not_mem_nil, or_false] at hp; subst hp + refine ⟨h1, fun hf => Or.inl ((h2 hf).resolve_right (by intro h; simp_all)), h3⟩ + · simp at hp + · split at hp + · simp only [List.mem_cons, List.not_mem_nil, or_false] at hp; subst hp + refine ⟨fun h => absurd (List.isEmpty_iff.mp (by assumption)) h, fun h => by simp at h, h3⟩ + · simp only [List.mem_cons, List.not_mem_nil, or_false] at hp; subst hp + exact ⟨h1, fun _ => Or.inl (by simp), h3⟩ + · simp only [List.mem_cons, List.not_mem_nil, or_false] at hp; subst hp + refine ⟨fun h => absurd rfl h, fun hf => Or.inl ((h2 hf).resolve_right (by intro h; simp_all)), + fun n hn => by simp [rootsVals_clear] at hn⟩ + · simp only [List.mem_cons, List.not_mem_nil, or_false] at hp; subst hp + obtain ⟨eb, ef, ej, _⟩ := rebuild_frame s + refine ⟨fun h => ?_, fun hf => ?_, fun n hn => Or.inl hn⟩ + · simp only [eb, ef] at h ⊢; exact h1 h + · simp only [ef, ej] at hf ⊢ + exact Or.inl ((h2 hf).resolve_right (by intro h; simp_all)) + · simp at hp + +theorem reach_inv (c : Cfg) (s : St) (h : Reach (Fixed.next false c) (St.init c) s) : Inv s := by + induction h with + | init => exact init_inv c + | step _ hmem ih => exact step_inv c _ ih _ hmem + +/-- Main theorem (all sizes): in the fixed design, whenever no UIUpdater is scheduled or + running, every root node in rootNodes is shown in the viewer. -/ +theorem no_lost_root (c : Cfg) (s : St) (h : Reach (Fixed.next false c) (St.init c) s) + (hj : s.jobs = 0) (hu : s.upc = .idle) : ∀ n ∈ rootsVals s.roots, n ∈ s.viewer := by + obtain ⟨h1, h2, h3⟩ := reach_inv c s h + have hf : s.flag = false := by + cases hfl : s.flag + · rfl + · rcases h2 hfl with h | h + · omega + · rw [hu] at h; cases h + have hb : s.batch = [] := by + cases hb : s.batch with + | nil => rfl + | cons x xs => + have := h1 (by rw [hb]; simp) + rw [this] at hf; cases hf + intro n hn + rcases h3 n hn with h | h + · exact h + · rw [hb] at h; cases h + +end FindRefs.Proof diff --git a/formal/find-refs/lean/FindRefs/State.lean b/formal/find-refs/lean/FindRefs/State.lean new file mode 100644 index 000000000..c4676698a --- /dev/null +++ b/formal/find-refs/lean/FindRefs/State.lean @@ -0,0 +1,152 @@ +/- +Shared state of the find-references model. + +Code under study (all line numbers refer to this file unless prefixed): + com.avaloq.tools.ddk.xtext.ui/src/com/avaloq/tools/ddk/xtext/ui/editor/findrefs/ + FastReferenceSearchResultContentProvider.java ("FRS:") +Xtext 2.44 org.eclipse.xtext.ui.editor.findrefs.ReferenceSearchResult ("RSR.") + +Actors + * S : the search job thread (Eclipse InternalSearchJob -> ReferenceQuery.run). + It calls RSR.reset() once at start and RSR.accept(ref) per match. + RSR.accept/reset mutate `matchingReferences` WITHOUT a lock and then call + RSR.fireEvent, which holds `synchronized(listeners)` while calling + FRS.searchResultChanged. => all event deliveries are serialised by the + `listeners` monitor (modelled by `lockS`). + * UI : the single SWT display thread. Each UI runnable (a UIJob body, a + syncExec runnable, a viewer.setInput -> inputChanged call) runs to + completion without interleaving with other UI runnables, but S steps + interleave freely between its individual shared-memory accesses. + * Jobs: `new UIUpdater().schedule()` / `schedule(250)` put a UIJob in the + job queue (`jobs` = number of scheduled-but-not-started instances). + A UIJob runs later as a UI runnable. + * Viewer: JFace TreeViewer. `refresh()` re-reads getElements() = rootNodes.values(), + so after refresh the root items are exactly the current map values. + `add` of an already present element is deduplicated (AbstractTreeViewer + itemExists). Children are fetched lazily => a reference is visible + iff it is attached to a root node that is shown (optimistic). + * Input: the viewer input is either the result A under study, or some other + result B (a different reference search shown in the same page). +-/ +import Std.Data.HashSet +import Std.Data.HashMap + +namespace FindRefs + +structure Cfg where + nU : Nat := 2 -- number of resource URIs + adds : Nat := 3 -- accept() calls available to S + resets : Nat := 1 -- reset() calls available to S (search (re)start) + switches : Nat := 2 -- page input switches A->B / B->A available to the user +deriving Repr + +/-- Search-thread program counter. `r` = reference id, `n` = node id. -/ +inductive SPc where + | idle + | fire (r : Nat) -- RSR.accept: matchingReferences.add done; fireEvent next + | get (r : Nat) -- FRS:158 rootNodes.get(uri) + | put (r : Nat) -- FRS:160-161 new node, rootNodes.put + | bat (r n : Nat) -- FRS:162-164 synchronized batchAddNodes.add + | child (r n : Nat) -- FRS:137 new DynamicReferenceSearchViewTreeNode(resourceNode, ..) + | flg -- FRS:173 read isUIUpdateScheduled + | setf -- FRS:174 isUIUpdateScheduled = true + | sched -- FRS:175 new UIUpdater().schedule(); then release `listeners` + | rfire -- RSR.reset: matchingReferences.clear done; fireEvent next + | rwait -- FRS:178 blocked in Display.syncExec +deriving BEq, Hashable, Repr, DecidableEq + +/-- UI-thread program counter (which UI runnable is mid-flight, and where). -/ +inductive UPc where + | idle + | uRefresh -- UIUpdater: FRS:216 viewer.refresh() next + | uCheck -- FRS:217 batchAddNodes.isEmpty() next + | uDecide (empty : Bool) -- FRS:217-221 reschedule or clear flag next + | uDecideF -- fixed model: atomic decide under batch lock + | wRemove -- inputChanged(A,B): cleared (FRS:111); removeListener(A) next (FRS:113) + | wFinish -- inputChanged(A,B): addListener(B) + setInput refresh + | bAdd -- inputChanged(B,A): cleared; removeListener(B), addListener(A) next (FRS:116) + | bIter -- FRS:118 getMatchingReferences().iterator() next + | bLoop (c m : Nat) -- FRS:118 for-each over live matchingReferences (cursor c, expected modCount m) + | bGet (c m r : Nat) -- FRS:119 -> 158 + | bPut (c m r : Nat) -- FRS:119 -> 160-161 + | bBat (c m r n : Nat) -- FRS:119 -> 162-164 + | bChild (c m r n : Nat) -- FRS:119 -> 137 + | bDone -- ContentViewer.setInput: input := A, refresh + | wFix -- fixed model: second half of inputChanged(A,B) + | bFix -- fixed model: second half of inputChanged(B,A) +deriving BEq, Hashable, Repr, DecidableEq + +inductive Inp where + | A | B +deriving BEq, Hashable, Repr, DecidableEq + +structure St where + spc : SPc := .idle + addB : Nat + resetB : Nat + switchB : Nat + lockS : Bool := false -- S holds RSR(A).listeners monitor + listening : Bool := true -- FRS registered as listener of A + matching : List Nat := [] -- RSR(A).matchingReferences + mc : Nat := 0 -- its ArrayList modCount + epoch : Nat := 0 -- number of reset() calls so far (ghost) + refs : List (Nat × Nat) := [] -- ref id ↦ (uri, epoch) (ghost) + nodes : List (Nat × Nat) := [] -- node id ↦ (uri, epoch of the ref that created it) (ghost) + roots : List (Option Nat) -- FRS.rootNodes : uri ↦ node + batch : List Nat := [] -- FRS.batchAddNodes + flag : Bool := false -- FRS.isUIUpdateScheduled + attach : List (Nat × Nat) := [] -- (ref, node): reference node attached under root node + jobs : Nat := 0 -- scheduled, not yet started UIUpdater instances + upc : UPc := .idle + syncReq : Bool := false -- Reset runnable posted by syncExec, not yet run + input : Inp := .A + viewer : List Nat := [] -- root items shown (sorted, dedup) + resetPending : Bool := false -- ghost: reset() called, effect not yet reflected in viewer + snap : Option (List Nat) := none -- UI-local snapshot (only used by the `snap` patch) + cme : Bool := false -- ConcurrentModificationException thrown on UI thread +deriving BEq, Hashable, Repr + +def St.init (c : Cfg) : St := + { addB := c.adds, resetB := c.resets, switchB := c.switches, roots := List.replicate c.nU none } + +/-! Helpers -/ + +def rootsVals (roots : List (Option Nat)) : List Nat := roots.filterMap id + +def getRoot (roots : List (Option Nat)) (u : Nat) : Option Nat := (roots[u]?).getD none + +def setRoot (roots : List (Option Nat)) (u : Nat) (v : Option Nat) : List (Option Nat) := roots.set u v + +def clearRoots (roots : List (Option Nat)) : List (Option Nat) := roots.map (fun _ => none) + +def sins (x : Nat) : List Nat → List Nat + | [] => [x] + | y :: ys => if x < y then x :: y :: ys else if x = y then y :: ys else y :: sins x ys + +def sset (l : List Nat) : List Nat := l.foldr sins [] + +def uriOfRef (s : St) (r : Nat) : Nat := ((s.refs[r]?).getD (0, 0)).1 +def epochOfRef (s : St) (r : Nat) : Nat := ((s.refs[r]?).getD (0, 0)).2 +def uriOfNode (s : St) (n : Nat) : Nat := ((s.nodes[n]?).getD (0, 0)).1 +def epochOfNode (s : St) (n : Nat) : Nat := ((s.nodes[n]?).getD (0, 0)).2 + +/-- Ghost bookkeeping for P3: a refresh only "reflects the last reset" when no Reset + event is still in flight to the provider. -/ +def resetInFlight (s : St) : Bool := s.spc == .rfire || s.spc == .rwait || s.syncReq + +/-- S idle: environment chooses the next RSR call (accept of a ref in uri u, or reset). -/ +def searchStarts (c : Cfg) (s : St) : List (String × St) := + (if s.addB > 0 then + (List.range c.nU).map fun u => + let r := s.refs.length + (s!"S RSR.accept(ref{r} in uri{u}): matchingReferences.add", + { s with addB := s.addB - 1, refs := s.refs ++ [(u, s.epoch)], matching := s.matching ++ [r], + mc := s.mc + 1, spc := .fire r }) + else []) ++ + (if s.resetB > 0 then + [("S RSR.reset(): matchingReferences.clear [search (re)started]", + { s with resetB := s.resetB - 1, matching := [], mc := s.mc + 1, epoch := s.epoch + 1, + resetPending := true, spc := .rfire })] + else []) + +end FindRefs diff --git a/formal/find-refs/lean/FindRefs/Theorems.lean b/formal/find-refs/lean/FindRefs/Theorems.lean new file mode 100644 index 000000000..33dac3d44 --- /dev/null +++ b/formal/find-refs/lean/FindRefs/Theorems.lean @@ -0,0 +1,36 @@ +/- +Bounded model-checking results as kernel-accepted theorems (native_decide over the +exhaustive BFS to a fixpoint). Default Cfg: 2 URIs, 3 accepts, 1 reset, 2 input switches. +-/ +import FindRefs.Buggy +import FindRefs.Fixed +import FindRefs.Check +import FindRefs.Proof + +namespace FindRefs.Theorems +open FindRefs + +def cfg : Cfg := {} + +/-- Verdict vector for a model: fixpoint reached, then for P1, P1', P2, P3, P4, DL whether it holds. -/ +def verdicts (next : St → List (String × St)) (c : Cfg) : List Bool := + let e := explore next (St.init c) + e.complete :: (props.map fun (_, p) => (firstViolation e p).isNone) ++ + [(firstViolation e (fun s => !deadlock next s)).isNone] + +/-- As written: P1, P1', P3, P4 and deadlock-freedom are violated; P2 holds. -/ +theorem buggy_verdicts : verdicts (Buggy.next .none cfg) cfg = [true, false, false, true, false, false, false] := by + native_decide + +/-- Fixed design: everything holds within the bound. -/ +theorem fixed_verdicts : verdicts (Fixed.next false cfg) cfg = [true, true, true, true, true, true, true] := by + native_decide + +/-- Sanity: a planted bug (flag set without scheduling) is caught (P1, P1'). -/ +theorem planted_caught : verdicts (Fixed.next true cfg) cfg = [true, false, false, true, true, true, true] := by + native_decide + +end FindRefs.Theorems + +#print axioms FindRefs.Proof.no_lost_root +#print axioms FindRefs.Theorems.fixed_verdicts diff --git a/formal/find-refs/lean/NOTES.md b/formal/find-refs/lean/NOTES.md new file mode 100644 index 000000000..63c07cbee --- /dev/null +++ b/formal/find-refs/lean/NOTES.md @@ -0,0 +1,188 @@ +# Find-references batching: Lean 4 model + +Subject: `com.avaloq.tools.ddk.xtext.ui/src/com/avaloq/tools/ddk/xtext/ui/editor/findrefs/FastReferenceSearchResultContentProvider.java` +(called **FRS** below; `FRS:n` is a line number). Context read: Xtext 2.44 `ReferenceSearchResult` (RSR), +`ReferenceQuery`, `ReferenceSearchViewPage`, superclass `ReferenceSearchResultContentProvider`; +Eclipse Search 3.19 `InternalSearchUI`, `SearchView`, `SearchViewManager`; JFace 3.40 `AbstractTreeViewer`. + +Toolchain: `leanprover/lean4:v4.35.0-rc2`, no Mathlib, no dependencies, nothing downloaded. + +``` +lake build # models, BFS checker, all-sizes proof, native_decide theorems (~65 s) +lake env lean Report.lean # every variant with shortest traces (~2 min 15 s); output saved in report.txt +``` + +| File | Lines | Contents | +|---|---|---| +| `FindRefs/State.lean` | 152 | state, pcs, helpers, environment (accept/reset choices) | +| `FindRefs/Buggy.lean` | 127 | the code as written, plus a patch ladder (`Patch`) | +| `FindRefs/Fixed.lean` | 82 | repaired design, plus `plant` (a deliberately planted bug) | +| `FindRefs/Check.lean` | 106 | BFS to a fixpoint, properties, shortest-trace extraction | +| `FindRefs/Proof.lean` | 203 | all-sizes inductive-invariant proof (no `sorry`) | +| `FindRefs/Theorems.lean` | 36 | `native_decide` verdict theorems + `#print axioms` | +| total | 723 | (plus `Report.lean`, 11) | + +## Threading assumptions + +* **Search thread S.** Eclipse `InternalSearchJob` runs `ReferenceQuery.run`, which calls `RSR.reset()` once and then `RSR.accept(ref)` once per match. There is one S per result: `InternalSearchUI.runSearchInBackground` refuses to start a query that is already running. + * `accept` and `reset` change `matchingReferences` (an `ArrayList`) with no lock. They then call `fireEvent`, which holds `synchronized(listeners)` while it calls `FRS.searchResultChanged`. + * So events reach FRS one at a time, and S holds the `listeners` monitor for the whole handler (`lockS`). +* **UI thread.** UI runnables (a UIJob body, a `syncExec` runnable, `setInput`→`inputChanged`) never interleave with each other. S steps can interleave between any two shared-memory accesses inside a UI runnable. + * `RSR.addListener` and `RSR.removeListener` are `synchronized(listeners)`, so the UI blocks on them while S is inside a handler. +* **UIJobs.** `new UIUpdater().schedule()` and `schedule(250)` add one pending instance (`jobs`), which runs later as a UI runnable. +* **Viewer (JFace).** `refresh()` rebuilds the root items from `getElements()` = `rootNodes.values()`. `add` of an element that is already present does nothing (`itemExists`). Children are fetched lazily, so a reference counts as visible if its root node is shown. This is an optimistic assumption. +* **Input switches (user).** The search page, viewer and FRS are one per view. `setInput(B)` for another reference-search result B calls `inputChanged(A,B)`, and showing A again calls `inputChanged(B,A)`. `page.setInput(null)` does not touch the viewer (`ReferenceSearchViewPage.setInput`), so it is not modelled. B is static (no search runs on it). +* **Memory model.** Sequential consistency (optimistic): the unsynchronized `batchAddNodes.isEmpty()` at FRS:217 and the `ArrayList` children are treated as SC. Under the real JMM things can only get worse. `ConcurrentHashMap` operations are atomic, and a refresh takes an atomic snapshot of the map. +* **Not modelled:** `descriptionsChanged` (index deltas), `dispose`, Removed/Finish events, races on the `children` list inside `ReferenceSearchViewTreeNode`. + +## Model + +State: S pc, the `listeners` lock, `listening`, `matchingReferences` and its modCount, `rootNodes` (uri ↦ node), `batchAddNodes`, `isUIUpdateScheduled`, scheduled job count, UI pc (with the locals of each UI runnable), pending `syncExec`, viewer input and root items, plus ghost data: ref/node → (uri, epoch), ref→node attachments, the reset epoch, `resetPending`, and `cme`. + +* Every access that is not atomic is its own step. For example, `rootNodes.get` (158), `put` (160-161), batch add (162-164), attach child (137), flag read (173), flag set (174) and schedule (175) are all separate. The UIUpdater's snapshot (207-215), refresh (216), `isEmpty` (217) and flag write/reschedule (218/220) are separate too. +* The `inputChanged` repopulation loop (118-120) walks the live list, with the `ArrayList.Itr` rules: `hasNext` is `cursor != size`, and `next` throws CME if modCount changed. +* Environment nondeterminism: S can pick `accept(ref in any uri)` or `reset()` within the budgets, and the user can switch A→B or B→A within the budget. +* Default bound: 2 URIs, 3 accepts, 1 reset, 2 switches. + +## Properties + +| Id | Statement | Checked where | +|---|---|---| +| P1 | No lost update. At quiescence (S idle, UI idle, no scheduled job, no pending `syncExec`, input A), every reference in `matchingReferences` is attached to a root node that is shown. | quiescent states | +| P1' | Root-level form of P1: at quiescence every node in `rootNodes` is shown. | quiescent states | +| P2 | One root per URI: no two shown root nodes have the same URI. | between UI runnables | +| P3 | No stale node. When input is B, nothing is shown. When input is A and no Reset is still in flight, every shown node belongs to the current epoch. | between UI runnables | +| P4 | No `ConcurrentModificationException` on the UI thread. | all states | +| DL | No deadlock: no state without successors while some actor is mid-flight. | all states | + +## Results + +| Model | States | Edges | P1 | P1' | P2 | P3 | P4 | DL | +|---|---|---|---|---|---|---|---|---| +| **as written** | 635,022 | 1,020,263 | ✗ (20) | ✗ (20) | ✓ | ✗ (12) | ✗ (8) | ✗ (3) | +| patch `lost` | 523,078 | 832,155 | ✗ (28) | ✓ | ✓ | ✗ (10) | ✗ (8) | ✗ (3) | +| patch `lost+order+snap` | 403,838 | 700,869 | ✗ (25) | ✓ | ✓ | ✓ | ✓ | ✗ (3) | +| patch `…+async` | 802,778 | 1,421,456 | ✗ (13) | ✓ | ✓ | ✓ | ✓ | ✓ | +| **fixed** | 9,952 | 16,835 | ✓ | ✓ | ✓ | ✓ | ✓ | ✓ | +| fixed, bound 3 URIs / 4 accepts / 2 resets / 3 switches | 1,892,441 | 3,418,927 | ✓ | ✓ | ✓ | ✓ | ✓ | ✓ | +| **fixed + planted bug** | 6,472 | 9,311 | ✗ (2) | ✗ (2) | ✓ | ✓ | ✓ | ✓ | + +✗ (k) = violated, with a shortest counterexample of k steps (BFS order). Every run reached a fixpoint. Full traces are in `report.txt`. + +### Proved and bounded-checked + +* **Proved for all sizes** (any number of URIs, accepts, resets, switches): `Proof.no_lost_root`. In every reachable state of the **fixed** model, if no UIUpdater is scheduled or running, every root node in `rootNodes` is shown (P1', the roots-level form). + * Inductive invariant: `batch ≠ [] → flag`, `flag → jobs > 0 ∨ UI at decide`, and `rootNodes.values ⊆ viewer ∪ batch`. + * Axioms: `propext` and `Quot.sound` only. +* **Kernel-checked bounded results** (`native_decide`, default bound): `Theorems.buggy_verdicts`, `fixed_verdicts` and `planted_caught` pin the verdict vectors in the table above. +* **Bounded only:** P1 (refs level), P2, P3, P4 and DL. + +### Sanity checks + +* The fixed model passes every property at both bounds. +* The planted bug (flag set without scheduling the job) is caught by P1/P1' in 2 steps. +* By construction, the planted bug also breaks clause 2 of the proof's invariant (flag set with no job). This is not separately proved. + +## Findings + +### F1: Lost update on the UIUpdater hand-off. **CONFIRMED** +Shortest trace (20 steps). Condensed from step 10 on, after node0 was delivered and a UIUpdater is scheduled: + +| # | Actor | Step | Code | +|---|---|---|---| +| 10-12 | S | `accept(ref1 in uri1)`, takes lock, `rootNodes.get(uri1)` = null | RSR.accept, FRS:170, FRS:158 | +| 13 | UI | UIUpdater snapshots and clears the batch [node0], `viewer.add` | FRS:207-215 | +| 14 | UI | `viewer.refresh()` | FRS:216 | +| 15 | S | `rootNodes.put(uri1, node1)` | FRS:160-161 | +| 16 | UI | `batchAddNodes.isEmpty()` = **true** | FRS:217 | +| 17-18 | S | `batchAddNodes.add(node1)`; attach ref1 | FRS:162-164, FRS:137 | +| 19 | S | `isUIUpdateScheduled == true`, so no schedule | FRS:173 | +| 20 | UI | `isUIUpdateScheduled = false` | FRS:220 | + +End state: node1 is in `rootNodes` and in the batch, but not in the viewer. The flag is false and no job exists. + +* Nothing brings node1 into the viewer until the next `Added` event. +* If this was the last match of the search, node1 never appears: the Finish event is ignored and nothing else refreshes the viewer. +* Why the Java does this: the "batch empty?" check at 217 and the flag clear at 220 are not atomic with S's batch add (162-164) and flag read (173). + +### F2: Deadlock between Reset's `syncExec` and `inputChanged`. **CONFIRMED** (timing window) + +| # | Actor | Step | Code | +|---|---|---|---| +| 1 | S | `reset()` | RSR.reset, from ReferenceQuery.run at job start | +| 2 | S | `fireEvent(Reset)` holds `A.listeners`, then `Display.syncExec` waits for the UI | FRS:178 | +| 3 | UI | `setInput(B)` → `inputChanged(A,B)` → `A.removeListener` blocks on `A.listeners` | FRS:113 | + +* How to trigger: the user starts another find-references (B) while A's job is starting. `InternalSearchUI.runSearchInBackground(B)` → `SearchViewManager.showNewSearchQuery` → `SearchView.showSearchResult` → `page.setInput(B)` runs on the UI thread. Picking another result from the search history also works. +* Result: S waits for the UI and the UI waits for S. The workbench freezes. +* Re-running A itself is safe, because `setInput(A)` happens before `job.schedule()`. +* The Xtext superclass has no `syncExec` and no such deadlock. + +### F3: Another search's in-flight node shown under result B. **CONFIRMED** +Shortest trace (12 steps): + +| # | Actor | Step | Code | +|---|---|---|---| +| 1-3 | S | `accept(ref0 in uri0)`, lock, `get(uri0)` = null | RSR.accept, FRS:170, FRS:158 | +| 4 | UI | `inputChanged(A,B)`: `rootNodes.clear()` | FRS:111 | +| 5-10 | S | `put(uri0, node0)`, batch add, attach, flag, schedule, release lock | FRS:160-175 | +| 11 | UI | `A.removeListener` (it was waiting for the lock) | FRS:113 | +| 12 | UI | `setInput(B)` refresh | FRS:216 semantics | + +End state: B's view shows A's node0. + +* Cause: the clear (111) comes before the listener removal (113). An A handler that is already in flight writes into the cleared map, which now belongs to B. +* If B is a fresh search, B's own Reset runnable removes the node shortly after, so it is transient. +* If B was picked from history (not re-run), the node stays for good: it is in `rootNodes`, and A's still-scheduled UIUpdater also refreshes it into view. + +### F4: CME on the UI thread in `inputChanged`. **CONFIRMED** +Shortest trace (8 steps): + +| # | Actor | Step | Code | +|---|---|---|---| +| 1-3 | UI | switch to B | | +| 4-5 | UI | switch back: `inputChanged(B,A)`, `A.addListener` | FRS:116 | +| 6 | UI | `getMatchingReferences().iterator()` | FRS:118 | +| 7 | S | `accept`: `matchingReferences.add`, no lock | RSR.accept | +| 8 | UI | `next()` throws `ConcurrentModificationException` out of `viewer.setInput` | FRS:118 | + +* How to trigger: switching the Search view back to a search that is still running. +* A `reset()` (`clear`) during the loop does the same. +* The Xtext superclass has the same live iteration. + +### F5: `resourceNode` check-then-act races the `inputChanged` repopulation. **CONFIRMED** +This was hidden behind F1. It showed up once F1 was patched (28 steps; see `report.txt`, section "patch: lost"). Every step in the trace behaves the same in the unpatched code. + +| # | Actor | Step | Code | +|---|---|---|---| +| — | S | `accept(ref1 in uri0)`: added to the list *before* A.addListener; fired *after* it | RSR.accept | +| 10 | S | `get(uri0)` = null | FRS:158 | +| 13-14 | UI | loop for ref0: `get(uri0)` = null; `put(uri0, node0)` | FRS:119→158, FRS:160-161 | +| 15-17 | S | `put(uri0, node1)` (overwrites node0); batch add; attach ref1→node1 | FRS:160-161, 162-164, 137 | +| 19-20 | UI | batch add node0; attach ref0→node0 | FRS:119 | +| 21-23 | UI | loop for ref1: `get(uri0)` = node1; attach ref1→node1 **again** | FRS:119 | + +End state: + +* Two root nodes were created for uri0. Only node1 is left in `rootNodes` and the viewer. +* ref0 hangs under the orphaned node0 and is never shown (P1 violated). +* ref1 is shown twice (duplicate row). +* Cause: FRS:158-161 is not atomic, and both the UI (inputChanged) and S call it. A reference that is accepted before the iterator is created but fired after `addListener` gets processed twice. +* Trigger: the same history-switch as F4, without the CME. + +### Observations (not violations) +* **Reset does not clear `batchAddNodes` (FRS:182-183).** The next UIUpdater re-adds pre-reset nodes at FRS:213. The full `refresh()` at FRS:216 removes them again inside the same UI runnable, so they are never visible: P3 holds on this path in every variant. The code is correct only because of that refresh. +* **P2 holds everywhere.** `rootNodes` is keyed by URI and every UI runnable ends with a full refresh. F5 still shows that two node objects can be created for one URI. +* **`asyncExec` alone is not a fix for F2.** Swapping `syncExec` for `asyncExec` removes the deadlock, but the Reset runnable then clears nodes added *after* the reset, which loses them (P1, 13 steps). The fixed design handles Reset on S under the provider lock. +* **Not modelled:** if `runInUIThread` throws (for example on a disposed viewer), `isUIUpdateScheduled` stays true for good and this FRS instance never schedules again. + +### Model artefact (found and fixed) +In the `lost+order+snap` variant, P3 first failed because the ghost `resetPending` was cleared at the end of `inputChanged`, even though a Reset event was still in flight. The real code would clear the node when that Reset arrived. The fix to the ghost: a refresh counts as reflecting the reset only when no Reset is in flight (`resetInFlight`). Verdict for that first trace: **MODEL-ARTEFACT**. No other violation above depends on ghost data except through P3, and F3's end state has input = B, which needs no ghost. + +## Fixed design (what `Fixed.lean` checks) +1. `addReference` / `resourceNode` and the flag test-and-set run atomically under one provider lock (dedupe: skip a ref already attached to the current root). UIUpdater's "batch empty ? clear flag : reschedule" runs under the same lock. +2. Reset is handled on S under that lock: clear `rootNodes` and the batch, and make sure an updater is scheduled. No `syncExec`. +3. `inputChanged` calls `removeListener` before clearing. On the way back it calls `addListener`, then snapshots and rebuilds under the provider lock and refreshes. + +## Wall time +About 27 minutes end to end: about 6 minutes reading code and framework sources, about 21 minutes modelling, checking, proving and writing. Machine time: `lake build` about 65 s, `Report.lean` about 2 min 15 s. diff --git a/formal/find-refs/lean/Report.lean b/formal/find-refs/lean/Report.lean new file mode 100644 index 000000000..3f76d4493 --- /dev/null +++ b/formal/find-refs/lean/Report.lean @@ -0,0 +1,11 @@ +import FindRefs +open FindRefs + +def cfg : Cfg := {} +#eval report "buggy (as written)" (Buggy.next .none cfg) (St.init cfg) +#eval report "patch: lost" (Buggy.next {lost := true} cfg) (St.init cfg) +#eval report "patch: lost+order+snap" (Buggy.next {lost := true, order := true, snap := true} cfg) (St.init cfg) +#eval report "patch: lost+order+snap+async" (Buggy.next {lost := true, order := true, snap := true, async := true} cfg) (St.init cfg) +#eval report "fixed" (Fixed.next false cfg) (St.init cfg) +#eval report "fixed + planted bug" (Fixed.next true cfg) (St.init cfg) +#eval report "fixed, larger bound nU=3 adds=4 resets=2 switches=3" (Fixed.next false {nU := 3, adds := 4, resets := 2, switches := 3}) (St.init {nU := 3, adds := 4, resets := 2, switches := 3}) diff --git a/formal/find-refs/lean/lake-manifest.json b/formal/find-refs/lean/lake-manifest.json new file mode 100644 index 000000000..172cc6ac5 --- /dev/null +++ b/formal/find-refs/lean/lake-manifest.json @@ -0,0 +1,6 @@ +{"version": "1.2.0", + "packagesDir": ".lake/packages", + "packages": [], + "name": "findrefs", + "lakeDir": ".lake", + "fixedToolchain": false} diff --git a/formal/find-refs/lean/lakefile.toml b/formal/find-refs/lean/lakefile.toml new file mode 100644 index 000000000..28dca5d38 --- /dev/null +++ b/formal/find-refs/lean/lakefile.toml @@ -0,0 +1,5 @@ +name = "findrefs" +defaultTargets = ["FindRefs"] + +[[lean_lib]] +name = "FindRefs" diff --git a/formal/find-refs/lean/lean-toolchain b/formal/find-refs/lean/lean-toolchain new file mode 100644 index 000000000..acc704ffe --- /dev/null +++ b/formal/find-refs/lean/lean-toolchain @@ -0,0 +1 @@ +leanprover/lean4:v4.35.0-rc2 diff --git a/formal/find-refs/lean/report.txt b/formal/find-refs/lean/report.txt new file mode 100644 index 000000000..03859074f --- /dev/null +++ b/formal/find-refs/lean/report.txt @@ -0,0 +1,221 @@ +== buggy (as written): 635022 states, 1020263 edges, fixpoint=true + P1 no lost update (refs): VIOLATED, shortest trace (20 steps): + 1. S RSR.accept(ref0 in uri0): matchingReferences.add + 2. S RSR.fireEvent(Added ref0) takes listeners lock -> FRS:170 + 3. S FRS:158 rootNodes.get(uri0) = null + 4. S FRS:160-161 rootNodes.put(uri0, node0) + 5. S FRS:162-164 batchAddNodes.add(node0) + 6. S FRS:137 attach ref0 under node0 + 7. S FRS:173 isUIUpdateScheduled == false + 8. S FRS:174 isUIUpdateScheduled = true + 9. S FRS:175 new UIUpdater().schedule(); release listeners lock + 10. S RSR.accept(ref1 in uri1): matchingReferences.add + 11. S RSR.fireEvent(Added ref1) takes listeners lock -> FRS:170 + 12. S FRS:158 rootNodes.get(uri1) = null + 13. UI UIUpdater starts: FRS:207-210 snapshot+clear batch [0]; FRS:212-215 viewer.add each + 14. UI FRS:216 viewer.refresh() (root items := rootNodes.values) + 15. S FRS:160-161 rootNodes.put(uri1, node1) + 16. UI FRS:217 batchAddNodes.isEmpty() = true + 17. S FRS:162-164 batchAddNodes.add(node1) + 18. S FRS:137 attach ref1 under node1 + 19. S FRS:173 isUIUpdateScheduled == true -> skip schedule; release listeners lock + 20. UI FRS:220 isUIUpdateScheduled = false + final: roots=[(some 0), (some 1)] batch=[1] flag=false jobs=0 viewer=[0] matching=[0, 1] attach=[(0, 0), (1, 1)] nodes=[(0, 0), (1, 0)] epoch=0 input=FindRefs.Inp.A spc=FindRefs.SPc.idle upc=FindRefs.UPc.idle lockS=false syncReq=false + P1' no lost update (roots): VIOLATED, shortest trace (20 steps): + 1. S RSR.accept(ref0 in uri0): matchingReferences.add + 2. S RSR.fireEvent(Added ref0) takes listeners lock -> FRS:170 + 3. S FRS:158 rootNodes.get(uri0) = null + 4. S FRS:160-161 rootNodes.put(uri0, node0) + 5. S FRS:162-164 batchAddNodes.add(node0) + 6. S FRS:137 attach ref0 under node0 + 7. S FRS:173 isUIUpdateScheduled == false + 8. S FRS:174 isUIUpdateScheduled = true + 9. S FRS:175 new UIUpdater().schedule(); release listeners lock + 10. S RSR.accept(ref1 in uri1): matchingReferences.add + 11. S RSR.fireEvent(Added ref1) takes listeners lock -> FRS:170 + 12. S FRS:158 rootNodes.get(uri1) = null + 13. UI UIUpdater starts: FRS:207-210 snapshot+clear batch [0]; FRS:212-215 viewer.add each + 14. UI FRS:216 viewer.refresh() (root items := rootNodes.values) + 15. S FRS:160-161 rootNodes.put(uri1, node1) + 16. UI FRS:217 batchAddNodes.isEmpty() = true + 17. S FRS:162-164 batchAddNodes.add(node1) + 18. S FRS:137 attach ref1 under node1 + 19. S FRS:173 isUIUpdateScheduled == true -> skip schedule; release listeners lock + 20. UI FRS:220 isUIUpdateScheduled = false + final: roots=[(some 0), (some 1)] batch=[1] flag=false jobs=0 viewer=[0] matching=[0, 1] attach=[(0, 0), (1, 1)] nodes=[(0, 0), (1, 0)] epoch=0 input=FindRefs.Inp.A spc=FindRefs.SPc.idle upc=FindRefs.UPc.idle lockS=false syncReq=false + P2 one root per URI: holds + P3 no stale node: VIOLATED, shortest trace (12 steps): + 1. S RSR.accept(ref0 in uri0): matchingReferences.add + 2. S RSR.fireEvent(Added ref0) takes listeners lock -> FRS:170 + 3. S FRS:158 rootNodes.get(uri0) = null + 4. UI user shows other result B: setInput(B) -> inputChanged(A,B) FRS:111 rootNodes.clear + 5. S FRS:160-161 rootNodes.put(uri0, node0) + 6. S FRS:162-164 batchAddNodes.add(node0) + 7. S FRS:137 attach ref0 under node0 + 8. S FRS:173 isUIUpdateScheduled == false + 9. S FRS:174 isUIUpdateScheduled = true + 10. S FRS:175 new UIUpdater().schedule(); release listeners lock + 11. UI FRS:113 A.removeListener(this) + 12. UI FRS:116 B.addListener; ContentViewer.setInput(B) refresh + final: roots=[(some 0), none] batch=[0] flag=true jobs=1 viewer=[0] matching=[0] attach=[(0, 0)] nodes=[(0, 0)] epoch=0 input=FindRefs.Inp.B spc=FindRefs.SPc.idle upc=FindRefs.UPc.idle lockS=false syncReq=false + P4 no UI-thread CME: VIOLATED, shortest trace (8 steps): + 1. UI user shows other result B: setInput(B) -> inputChanged(A,B) FRS:111 rootNodes.clear + 2. UI FRS:113 A.removeListener(this) + 3. UI FRS:116 B.addListener; ContentViewer.setInput(B) refresh + 4. UI user shows result A again: setInput(A) -> inputChanged(B,A) FRS:111 rootNodes.clear + 5. UI FRS:116 A.addListener(this) + 6. UI FRS:118 matchingReferences.iterator() + 7. S RSR.accept(ref0 in uri0): matchingReferences.add + 8. UI FRS:118 iterator.next() throws ConcurrentModificationException + final: roots=[none, none] batch=[] flag=false jobs=0 viewer=[] matching=[0] attach=[] nodes=[] epoch=0 input=FindRefs.Inp.B spc=FindRefs.SPc.fire 0 upc=FindRefs.UPc.idle lockS=false syncReq=false + DL no deadlock: VIOLATED, shortest trace (3 steps): + 1. S RSR.reset(): matchingReferences.clear [search (re)started] + 2. S RSR.fireEvent(Reset) takes listeners lock -> FRS:178 Display.syncExec (blocks) + 3. UI user shows other result B: setInput(B) -> inputChanged(A,B) FRS:111 rootNodes.clear + final: roots=[none, none] batch=[] flag=false jobs=0 viewer=[] matching=[] attach=[] nodes=[] epoch=1 input=FindRefs.Inp.A spc=FindRefs.SPc.rwait upc=FindRefs.UPc.wRemove lockS=true syncReq=true +== patch: lost: 523078 states, 832155 edges, fixpoint=true + P1 no lost update (refs): VIOLATED, shortest trace (28 steps): + 1. S RSR.accept(ref0 in uri0): matchingReferences.add + 2. UI user shows other result B: setInput(B) -> inputChanged(A,B) FRS:111 rootNodes.clear + 3. UI FRS:113 A.removeListener(this) + 4. S RSR.fireEvent(Added ref0): FRS not a listener, dropped + 5. S RSR.accept(ref1 in uri0): matchingReferences.add + 6. UI FRS:116 B.addListener; ContentViewer.setInput(B) refresh + 7. UI user shows result A again: setInput(A) -> inputChanged(B,A) FRS:111 rootNodes.clear + 8. UI FRS:116 A.addListener(this) + 9. S RSR.fireEvent(Added ref1) takes listeners lock -> FRS:170 + 10. S FRS:158 rootNodes.get(uri0) = null + 11. UI FRS:118 matchingReferences.iterator() + 12. UI FRS:118 next() = ref0 + 13. UI FRS:119->158 rootNodes.get(uri0) = null + 14. UI FRS:119->160-161 rootNodes.put(uri0, node0) + 15. S FRS:160-161 rootNodes.put(uri0, node1) + 16. S FRS:162-164 batchAddNodes.add(node1) + 17. S FRS:137 attach ref1 under node1 + 18. S [patched] synchronized(batch){flag := true; schedule}; release listeners lock + 19. UI FRS:119->162-164 batchAddNodes.add(node0) + 20. UI FRS:119->137 attach ref0 under node0 + 21. UI FRS:118 next() = ref1 + 22. UI FRS:119->158 rootNodes.get(uri0) = node1 + 23. UI FRS:119->137 attach ref1 under node1 + 24. UI FRS:118 iterator.hasNext() = false + 25. UI ContentViewer.setInput(A): input := A; refresh + 26. UI UIUpdater starts: FRS:207-210 snapshot+clear batch [1, 0]; FRS:212-215 viewer.add each + 27. UI FRS:216 viewer.refresh() (root items := rootNodes.values) + 28. UI [patched] synchronized(batch){empty -> flag := false} + final: roots=[(some 1), none] batch=[] flag=false jobs=0 viewer=[1] matching=[0, 1] attach=[(1, 1), (0, 0), (1, 1)] nodes=[(0, 0), (0, 0)] epoch=0 input=FindRefs.Inp.A spc=FindRefs.SPc.idle upc=FindRefs.UPc.idle lockS=false syncReq=false + P1' no lost update (roots): holds + P2 one root per URI: holds + P3 no stale node: VIOLATED, shortest trace (10 steps): + 1. S RSR.accept(ref0 in uri0): matchingReferences.add + 2. S RSR.fireEvent(Added ref0) takes listeners lock -> FRS:170 + 3. S FRS:158 rootNodes.get(uri0) = null + 4. UI user shows other result B: setInput(B) -> inputChanged(A,B) FRS:111 rootNodes.clear + 5. S FRS:160-161 rootNodes.put(uri0, node0) + 6. S FRS:162-164 batchAddNodes.add(node0) + 7. S FRS:137 attach ref0 under node0 + 8. S [patched] synchronized(batch){flag := true; schedule}; release listeners lock + 9. UI FRS:113 A.removeListener(this) + 10. UI FRS:116 B.addListener; ContentViewer.setInput(B) refresh + final: roots=[(some 0), none] batch=[0] flag=true jobs=1 viewer=[0] matching=[0] attach=[(0, 0)] nodes=[(0, 0)] epoch=0 input=FindRefs.Inp.B spc=FindRefs.SPc.idle upc=FindRefs.UPc.idle lockS=false syncReq=false + P4 no UI-thread CME: VIOLATED, shortest trace (8 steps): + 1. UI user shows other result B: setInput(B) -> inputChanged(A,B) FRS:111 rootNodes.clear + 2. UI FRS:113 A.removeListener(this) + 3. UI FRS:116 B.addListener; ContentViewer.setInput(B) refresh + 4. UI user shows result A again: setInput(A) -> inputChanged(B,A) FRS:111 rootNodes.clear + 5. UI FRS:116 A.addListener(this) + 6. UI FRS:118 matchingReferences.iterator() + 7. S RSR.accept(ref0 in uri0): matchingReferences.add + 8. UI FRS:118 iterator.next() throws ConcurrentModificationException + final: roots=[none, none] batch=[] flag=false jobs=0 viewer=[] matching=[0] attach=[] nodes=[] epoch=0 input=FindRefs.Inp.B spc=FindRefs.SPc.fire 0 upc=FindRefs.UPc.idle lockS=false syncReq=false + DL no deadlock: VIOLATED, shortest trace (3 steps): + 1. S RSR.reset(): matchingReferences.clear [search (re)started] + 2. S RSR.fireEvent(Reset) takes listeners lock -> FRS:178 Display.syncExec (blocks) + 3. UI user shows other result B: setInput(B) -> inputChanged(A,B) FRS:111 rootNodes.clear + final: roots=[none, none] batch=[] flag=false jobs=0 viewer=[] matching=[] attach=[] nodes=[] epoch=1 input=FindRefs.Inp.A spc=FindRefs.SPc.rwait upc=FindRefs.UPc.wRemove lockS=true syncReq=true +== patch: lost+order+snap: 403838 states, 700869 edges, fixpoint=true + P1 no lost update (refs): VIOLATED, shortest trace (25 steps): + 1. S RSR.accept(ref0 in uri0): matchingReferences.add + 2. UI [patched] user shows other result B: inputChanged(A,B) removeListener first + 3. UI [patched] A.removeListener(this); rootNodes.clear + 4. S RSR.fireEvent(Added ref0): FRS not a listener, dropped + 5. UI FRS:116 B.addListener; ContentViewer.setInput(B) refresh + 6. UI user shows result A again: setInput(A) -> inputChanged(B,A) FRS:111 rootNodes.clear + 7. UI FRS:116 A.addListener(this) + 8. UI [patched] snapshot = copy of matchingReferences + 9. S RSR.accept(ref1 in uri0): matchingReferences.add + 10. S RSR.fireEvent(Added ref1) takes listeners lock -> FRS:170 + 11. S FRS:158 rootNodes.get(uri0) = null + 12. UI FRS:118 next() = ref0 + 13. UI FRS:119->158 rootNodes.get(uri0) = null + 14. S FRS:160-161 rootNodes.put(uri0, node0) + 15. S FRS:162-164 batchAddNodes.add(node0) + 16. S FRS:137 attach ref1 under node0 + 17. S [patched] synchronized(batch){flag := true; schedule}; release listeners lock + 18. UI FRS:119->160-161 rootNodes.put(uri0, node1) + 19. UI FRS:119->162-164 batchAddNodes.add(node1) + 20. UI FRS:119->137 attach ref0 under node1 + 21. UI FRS:118 iterator.hasNext() = false + 22. UI ContentViewer.setInput(A): input := A; refresh + 23. UI UIUpdater starts: FRS:207-210 snapshot+clear batch [0, 1]; FRS:212-215 viewer.add each + 24. UI FRS:216 viewer.refresh() (root items := rootNodes.values) + 25. UI [patched] synchronized(batch){empty -> flag := false} + final: roots=[(some 1), none] batch=[] flag=false jobs=0 viewer=[1] matching=[0, 1] attach=[(1, 0), (0, 1)] nodes=[(0, 0), (0, 0)] epoch=0 input=FindRefs.Inp.A spc=FindRefs.SPc.idle upc=FindRefs.UPc.idle lockS=false syncReq=false + P1' no lost update (roots): holds + P2 one root per URI: holds + P3 no stale node: holds + P4 no UI-thread CME: holds + DL no deadlock: VIOLATED, shortest trace (3 steps): + 1. S RSR.reset(): matchingReferences.clear [search (re)started] + 2. S RSR.fireEvent(Reset) takes listeners lock -> FRS:178 Display.syncExec (blocks) + 3. UI [patched] user shows other result B: inputChanged(A,B) removeListener first + final: roots=[none, none] batch=[] flag=false jobs=0 viewer=[] matching=[] attach=[] nodes=[] epoch=1 input=FindRefs.Inp.A spc=FindRefs.SPc.rwait upc=FindRefs.UPc.wRemove lockS=true syncReq=true +== patch: lost+order+snap+async: 802778 states, 1421456 edges, fixpoint=true + P1 no lost update (refs): VIOLATED, shortest trace (13 steps): + 1. S RSR.reset(): matchingReferences.clear [search (re)started] + 2. S [patched] RSR.fireEvent(Reset) -> Display.asyncExec (no wait) + 3. S RSR.accept(ref0 in uri0): matchingReferences.add + 4. S RSR.fireEvent(Added ref0) takes listeners lock -> FRS:170 + 5. S FRS:158 rootNodes.get(uri0) = null + 6. S FRS:160-161 rootNodes.put(uri0, node0) + 7. S FRS:162-164 batchAddNodes.add(node0) + 8. S FRS:137 attach ref0 under node0 + 9. S [patched] synchronized(batch){flag := true; schedule}; release listeners lock + 10. UI UIUpdater starts: FRS:207-210 snapshot+clear batch [0]; FRS:212-215 viewer.add each + 11. UI FRS:216 viewer.refresh() (root items := rootNodes.values) + 12. UI [patched] synchronized(batch){empty -> flag := false} + 13. UI Reset runnable FRS:181-186: viewer.remove(rootNodes.values), rootNodes.clear, refresh + final: roots=[none, none] batch=[] flag=false jobs=0 viewer=[] matching=[0] attach=[(0, 0)] nodes=[(0, 1)] epoch=1 input=FindRefs.Inp.A spc=FindRefs.SPc.idle upc=FindRefs.UPc.idle lockS=false syncReq=false + P1' no lost update (roots): holds + P2 one root per URI: holds + P3 no stale node: holds + P4 no UI-thread CME: holds + DL no deadlock: holds +== fixed: 9952 states, 16835 edges, fixpoint=true + P1 no lost update (refs): holds + P1' no lost update (roots): holds + P2 one root per URI: holds + P3 no stale node: holds + P4 no UI-thread CME: holds + DL no deadlock: holds +== fixed + planted bug: 6472 states, 9311 edges, fixpoint=true + P1 no lost update (refs): VIOLATED, shortest trace (2 steps): + 1. S RSR.accept(ref0 in uri0): matchingReferences.add + 2. S fireEvent(Added ref0) -> atomic addReference + final: roots=[(some 0), none] batch=[0] flag=true jobs=0 viewer=[] matching=[0] attach=[(0, 0)] nodes=[(0, 0)] epoch=0 input=FindRefs.Inp.A spc=FindRefs.SPc.idle upc=FindRefs.UPc.idle lockS=false syncReq=false + P1' no lost update (roots): VIOLATED, shortest trace (2 steps): + 1. S RSR.accept(ref0 in uri0): matchingReferences.add + 2. S fireEvent(Added ref0) -> atomic addReference + final: roots=[(some 0), none] batch=[0] flag=true jobs=0 viewer=[] matching=[0] attach=[(0, 0)] nodes=[(0, 0)] epoch=0 input=FindRefs.Inp.A spc=FindRefs.SPc.idle upc=FindRefs.UPc.idle lockS=false syncReq=false + P2 one root per URI: holds + P3 no stale node: holds + P4 no UI-thread CME: holds + DL no deadlock: holds +== fixed, larger bound nU=3 adds=4 resets=2 switches=3: 1892441 states, 3418927 edges, fixpoint=true + P1 no lost update (refs): holds + P1' no lost update (roots): holds + P2 one root per URI: holds + P3 no stale node: holds + P4 no UI-thread CME: holds + DL no deadlock: holds +lake env lean Report.lean 130.83s user 0.71s system 99% cpu 2:12.56 total diff --git a/formal/find-refs/lean/theorems.txt b/formal/find-refs/lean/theorems.txt new file mode 100644 index 000000000..120074587 --- /dev/null +++ b/formal/find-refs/lean/theorems.txt @@ -0,0 +1,16 @@ +# ; checked by formal/check.sh via #print axioms +FindRefs.Proof.addRef_inv kernel +FindRefs.Proof.attachRef_cover kernel +FindRefs.Proof.attachRef_frame kernel +FindRefs.Proof.ensureScheduled_inv kernel +FindRefs.Proof.init_inv kernel +FindRefs.Proof.no_lost_root kernel +FindRefs.Proof.reach_inv kernel +FindRefs.Proof.rebuild_frame kernel +FindRefs.Proof.rootsVals_clear kernel +FindRefs.Proof.rootsVals_set kernel +FindRefs.Proof.searchStarts_frame kernel +FindRefs.Proof.step_inv kernel +FindRefs.Theorems.buggy_verdicts native_decide +FindRefs.Theorems.fixed_verdicts native_decide +FindRefs.Theorems.planted_caught native_decide diff --git a/formal/find-refs/tla/FindRefs.cfg b/formal/find-refs/tla/FindRefs.cfg new file mode 100644 index 000000000..7ffe551ab --- /dev/null +++ b/formal/find-refs/tla/FindRefs.cfg @@ -0,0 +1,15 @@ +\* Original code. Checks the three requested properties plus the extras; TLC stops at the first +\* violation (use run.sh / matrix.sh for one-property-per-run shortest traces). +SPECIFICATION Spec +CONSTANTS + Refs <- DefaultRefs + Fixes <- NoFixes + Planted = FALSE + MaxRuns = 2 + MaxSwitch = 2 +INVARIANTS + TypeOK + NoLostRoot NoLostRef + OneRootPerUri OneRootCreated NoDupRef + NoStale NoForeign + NoCME NoDeadlock diff --git a/formal/find-refs/tla/FindRefs.tla b/formal/find-refs/tla/FindRefs.tla new file mode 100644 index 000000000..1401255ac --- /dev/null +++ b/formal/find-refs/tla/FindRefs.tla @@ -0,0 +1,483 @@ +------------------------------ MODULE FindRefs ------------------------------ +(***************************************************************************) +(* Model of FastReferenceSearchResultContentProvider (FRSRCP) together *) +(* with the Xtext ReferenceSearchResult R it listens to, the search job *) +(* thread, the SWT UI thread (UIJob + syncExec/asyncExec runnables + user *) +(* view switches) and the JFace TreeViewer's root items. *) +(* *) +(* Line refs: FRSRCP = FastReferenceSearchResultContentProvider.java, *) +(* RSR = xtext ReferenceSearchResult.java, *) +(* RSVP = xtext ReferenceSearchViewPage.java. *) +(* *) +(* Fixes = {} is the code as written; each element enables one minimal *) +(* fix (see NOTES.md). Planted = TRUE plants an obvious bug on top. *) +(* *) +(***************************************************************************) +EXTENDS Naturals, Sequences, FiniteSets, TLC + +CONSTANTS Refs, \* resource URI of each reference the search delivers, in order + MaxRuns, \* number of search runs (>1 = "Search Again", i.e. Reset on a live provider) + MaxSwitch, \* number of user view switches R->B / B->R (B = another, finished search) + Fixes, \* subset of AllFixes + Planted \* planted bug: the Added handler never schedules the UIUpdater + +AllFixes == {"flag", "atomic", "dedupe", "snapshot", "reset", "plock", "detach"} +ASSUME Fixes \subseteq AllFixes /\ Planted \in BOOLEAN + +Fix(x) == x \in Fixes + +\* Defaults for FindRefs.cfg / FindRefsFixed.cfg (cfg files cannot hold sequences) +DefaultRefs == <<"u1", "u2">> +NoFixes == {} +MinFixes == {"flag", "dedupe", "snapshot", "reset", "plock", "detach"} +URIs == {Refs[k] : k \in DOMAIN Refs} +Nil == 0 +RefUri(ref) == Refs[ref[2]] \* a reference is <> +Range(f) == {f[x] : x \in DOMAIN f} + +VARIABLES + \* --- ReferenceSearchResult R (Xtext) --- + matching, \* R.matchingReferences (ArrayList, unsynchronized) + matchMod, \* its modCount + provReg, \* provider \in R.listeners + lockL, \* monitor of R.listeners: "none" | "S" | "U" + lockP, \* (fix "plock") provider-private monitor: "none" | "S" | "U" + \* --- provider state --- + rootNodes, \* URI -> node id (ConcurrentMap), Nil = absent + batch, \* batchAddNodes + flag, \* isUIUpdateScheduled + nodes, \* heap of ReferenceSearchViewTreeNode: [uri, ep, kids, gen] + clears, \* number of rootNodes.clear() so far (node.gen = clears at creation) + \* --- Display / Jobs --- + jobs, \* number of pending UIUpdater executions + syncPending, \* Reset runnable posted by syncExec, not yet run + asyncQ, \* (fixed) posted asyncExec refresh runnables (epochs) + \* --- viewer --- + shown, \* node ids that are root items of the TreeViewer + view, \* result the page shows: "R" | "B" + provEpoch, \* epoch of the last Reset / inputChanged the viewer has processed + \* --- search thread --- + pcS, iS, epoch, runs, sNode, + \* --- UI thread --- + pcU, uNonEmpty, uCur, uExp, uSnap, uRef, uNode, cme, switches + +vars == <> + +EmptyMap == [u \in URIs |-> Nil] +RootSet(rn) == Range(rn) \ {Nil} +NewNode(u) == [uri |-> u, ep |-> epoch, kids |-> <<>>, gen |-> clears] +HasKid(n, ref) == \E j \in DOMAIN nodes[n].kids : nodes[n].kids[j] = ref +AddKid(ns, n, ref) == \* new DynamicReferenceSearchViewTreeNode(parent, ...) -> parent.addChild + IF Fix("dedupe") /\ \E j \in DOMAIN ns[n].kids : ns[n].kids[j] = ref THEN ns \* fix: dedupe + ELSE [ns EXCEPT ![n].kids = Append(@, ref)] + +Init == + /\ matching = <<>> /\ matchMod = 0 + /\ provReg = TRUE \* page showed R (setInput) before the job was scheduled + /\ lockL = "none" /\ lockP = "none" + /\ rootNodes = EmptyMap /\ batch = <<>> /\ flag = FALSE /\ nodes = <<>> /\ clears = 0 + /\ jobs = 0 /\ syncPending = FALSE /\ asyncQ = <<>> + /\ shown = {} /\ view = "R" /\ provEpoch = 0 + /\ pcS = "sched" /\ iS = 0 /\ epoch = 0 /\ runs = 1 /\ sNode = Nil + /\ pcU = "idle" /\ uNonEmpty = FALSE /\ uCur = 0 /\ uExp = 0 /\ uSnap = <<>> + /\ uRef = <<0, 0>> /\ uNode = Nil /\ cme = FALSE /\ switches = 0 + +UVars == <> +UVarsNoC == <> +UVarsNoP == <> +SVars == <> + +(***************************************************************************) +(* Search job thread (InternalSearchJob -> ReferenceQuery.run). *) +(***************************************************************************) +SJobStart == \* job picked up by a worker + /\ pcS = "sched" /\ pcS' = "reset" + /\ UNCHANGED <> + +SReset == \* RSR:104 matchingReferences.clear() + /\ pcS = "reset" + /\ matching' = <<>> /\ matchMod' = matchMod + 1 /\ epoch' = epoch + 1 + /\ pcS' = "rlock" + /\ UNCHANGED <> + +SResetLock == \* RSR:54 synchronized(listeners) -> FRSRCP:177 Reset handler + /\ pcS = "rlock" /\ lockL = "none" /\ lockL' = "S" + /\ IF provReg /\ ~Fix("reset") + THEN /\ syncPending' = TRUE /\ pcS' = "rwait" \* FRSRCP:178 syncExec (blocks) + /\ UNCHANGED <> + ELSE IF provReg /\ Fix("reset") + THEN \* fix: clear model on the search thread, asyncExec only the viewer refresh + /\ pcS' = "rclear" /\ UNCHANGED <> + ELSE /\ pcS' = "runlock" /\ UNCHANGED <> + /\ UNCHANGED <> + +SRClear == \* fix "reset": clear model on the search thread (under the provider lock if "plock"), + \* and asyncExec only the viewer refresh + /\ pcS = "rclear" /\ (Fix("plock") => lockP = "none") + /\ rootNodes' = EmptyMap /\ clears' = clears + 1 /\ batch' = <<>> /\ asyncQ' = Append(asyncQ, epoch) /\ pcS' = "runlock" + /\ UNCHANGED <> + +SResetWait == \* syncExec returns once the UI thread ran the runnable + /\ pcS = "rwait" /\ ~syncPending /\ pcS' = "runlock" + /\ UNCHANGED <> + +SResetUnlock == + /\ pcS = "runlock" /\ lockL' = "none" + /\ iS' = 1 /\ pcS' = IF Len(Refs) >= 1 THEN "acc" ELSE "fin" + /\ UNCHANGED <> + +SAccept == \* RSR:85 matchingReferences.add (outside the listeners lock) + /\ pcS = "acc" + /\ matching' = Append(matching, <>) /\ matchMod' = matchMod + 1 + /\ pcS' = "lock" + /\ UNCHANGED <> + +SLock == \* RSR:54-56 fireEvent(Added): lock, deliver to provider if registered + /\ pcS = "lock" /\ lockL = "none" /\ lockL' = "S" + /\ pcS' = IF provReg THEN (IF Fix("plock") THEN "plk" ELSE "get") ELSE "unlock" + /\ UNCHANGED <> + +SPLock == \* fix "plock": synchronized (providerLock) around the Added handler body + /\ pcS = "plk" /\ lockP = "none" /\ lockP' = "S" /\ pcS' = "get" + /\ UNCHANGED <> + +SGet == \* FRSRCP:158-160 rootNodes.get; if null new node (fix "atomic": computeIfAbsent; subsumed by "plock") + /\ pcS = "get" + /\ LET u == Refs[iS] IN + IF rootNodes[u] # Nil + THEN /\ sNode' = rootNodes[u] /\ pcS' = "child" + /\ UNCHANGED <> + ELSE /\ nodes' = Append(nodes, NewNode(u)) /\ sNode' = Len(nodes) + 1 + /\ IF Fix("atomic") + THEN /\ rootNodes' = [rootNodes EXCEPT ![u] = Len(nodes) + 1] + /\ batch' = Append(batch, Len(nodes) + 1) /\ pcS' = "child" + ELSE /\ pcS' = "put" /\ UNCHANGED <> + /\ UNCHANGED <> + +SPut == \* FRSRCP:161 rootNodes.put + /\ pcS = "put" /\ rootNodes' = [rootNodes EXCEPT ![Refs[iS]] = sNode] /\ pcS' = "batch" + /\ UNCHANGED <> + +SBatch == \* FRSRCP:162-164 batchAddNodes.add (under its own lock -> atomic) + /\ pcS = "batch" /\ batch' = Append(batch, sNode) /\ pcS' = "child" + /\ UNCHANGED <> + +SChild == \* FRSRCP:137 new DynamicReferenceSearchViewTreeNode(resourceNode, ...) -> addChild + /\ pcS = "child" /\ nodes' = AddKid(nodes, sNode, <>) /\ pcS' = "flag" + /\ UNCHANGED <> + +SFlag == \* FRSRCP:173 if (!isUIUpdateScheduled) + /\ pcS = "flag" + /\ pcS' = IF flag \/ Planted THEN "unlock" ELSE "setflag" + /\ UNCHANGED <> + +SSetFlag == \* FRSRCP:174 + /\ pcS = "setflag" /\ flag' = TRUE /\ pcS' = "sched2" + /\ UNCHANGED <> + +SSchedule == \* FRSRCP:175 new UIUpdater().schedule() + /\ pcS = "sched2" /\ jobs' = jobs + 1 /\ pcS' = "unlock" + /\ UNCHANGED <> + +SUnlock == \* RSR:57 end of fireEvent + /\ pcS = "unlock" /\ lockL' = "none" /\ lockP' = IF lockP = "S" THEN "none" ELSE lockP + /\ IF iS < Len(Refs) THEN iS' = iS + 1 /\ pcS' = "acc" ELSE pcS' = "fin" /\ UNCHANGED iS + /\ UNCHANGED <> + +SFinish == \* RSR:109 fireEvent(Finish): provider ignores it; lock taken and released + /\ pcS = "fin" /\ lockL = "none" /\ pcS' = "done" + /\ UNCHANGED <> + +SearchStep == SJobStart \/ SReset \/ SResetLock \/ SResetWait \/ SResetUnlock \/ SAccept + \/ SLock \/ SGet \/ SPut \/ SBatch \/ SChild \/ SFlag \/ SSetFlag \/ SSchedule \/ SUnlock \/ SFinish \/ SRClear \/ SPLock + +(***************************************************************************) +(* UI thread. Only one runnable / event handler runs at a time; picks any *) +(* pending one when idle. *) +(***************************************************************************) +Unchanged_S_R == UNCHANGED <> + +UIRunSyncReset == \* FRSRCP:180-186 on the UI thread + /\ pcU = "idle" /\ syncPending + /\ shown' = {} \* remove(input, rootNodes.values); rootNodes.clear; refresh -> getElements = {} + /\ rootNodes' = EmptyMap /\ clears' = clears + 1 /\ syncPending' = FALSE /\ provEpoch' = epoch + /\ UNCHANGED <> + /\ UNCHANGED <> + +UIRunAsyncReset == \* (fixed only) asyncExec'd viewer.refresh after Reset + /\ pcU = "idle" /\ asyncQ # <<>> + /\ shown' = RootSet(rootNodes) /\ provEpoch' = Head(asyncQ) /\ asyncQ' = Tail(asyncQ) + /\ UNCHANGED <> + /\ Unchanged_S_R + +UIJobStart == \* UIJob -> Display.asyncExec(runInUIThread) + /\ pcU = "idle" /\ jobs > 0 /\ jobs' = jobs - 1 + /\ pcU' = IF Fix("flag") THEN "u_clr" ELSE "u_drain" + /\ UNCHANGED <> + /\ Unchanged_S_R + +UClear == \* (fixed) isUIUpdateScheduled = false first, as upstream Xtext does + /\ pcU = "u_clr" /\ flag' = FALSE /\ pcU' = "u_drain" + /\ UNCHANGED <> + /\ Unchanged_S_R + +UDrain == \* FRSRCP:207-215 copy+clear batch under lock, viewer.add each + /\ pcU = "u_drain" + /\ shown' = shown \cup Range(batch) /\ batch' = <<>> /\ pcU' = "u_refresh" + /\ UNCHANGED <> + /\ Unchanged_S_R + +URefresh == \* FRSRCP:216 viewer.refresh() -> getElements() = rootNodes.values() + /\ pcU = "u_refresh" + /\ shown' = RootSet(rootNodes) /\ pcU' = IF Fix("flag") THEN "idle" ELSE "u_check" + /\ UNCHANGED <> + /\ Unchanged_S_R + +UCheck == \* FRSRCP:217 !batchAddNodes.isEmpty() (unsynchronized read) + /\ pcU = "u_check" /\ uNonEmpty' = (batch # <<>>) /\ pcU' = "u_end" + /\ UNCHANGED <> + /\ Unchanged_S_R + +UEnd == \* FRSRCP:218 schedule(250) / 220 isUIUpdateScheduled = false + /\ pcU = "u_end" + /\ IF uNonEmpty THEN jobs' = jobs + 1 /\ UNCHANGED flag + ELSE flag' = FALSE /\ UNCHANGED jobs + /\ pcU' = "idle" + /\ UNCHANGED <> + /\ Unchanged_S_R + +\* ---- user: "Search Again" on R (SearchAgainAction -> runQueryInBackground; addQuery is a no-op) ---- +UserRerun == + /\ pcU = "idle" /\ view = "R" /\ pcS = "done" /\ runs < MaxRuns + /\ pcS' = "sched" /\ runs' = runs + 1 + /\ UNCHANGED <> + +\* ---- user: switch the view to another (finished) search B, e.g. from history ---- +\* SearchView.internalShowSearchPage: page.setInput(null) ; page.setInput(B) +UserToB == + /\ pcU = "idle" /\ view = "R" /\ switches < MaxSwitch + /\ pcU' = "b_disp" /\ switches' = switches + 1 + /\ UNCHANGED <> + /\ Unchanged_S_R + +UBDisp == \* event dispatch / getUIState before touching R + /\ pcU = "b_disp" /\ pcU' = "b_lbl" + /\ UNCHANGED <> + /\ Unchanged_S_R + +UBLabel == \* RSVP:139 R.removeListener(labelUpdater): needs R.listeners monitor + /\ pcU = "b_lbl" /\ lockL = "none" + /\ pcU' = IF Fix("detach") THEN "b_rm" ELSE "b_clear" + /\ UNCHANGED <> + /\ Unchanged_S_R + +UBClear == \* FRSRCP:111 rootNodes.clear() + /\ pcU = "b_clear" /\ (Fix("plock") => lockP = "none") /\ rootNodes' = EmptyMap /\ clears' = clears + 1 + /\ pcU' = IF Fix("detach") THEN "b_ref" ELSE "b_rm" + /\ UNCHANGED <> + /\ UNCHANGED <> + +UBRemove == \* FRSRCP:113 R.removeListener(this); fix: done before the clear + /\ pcU = "b_rm" /\ lockL = "none" /\ provReg' = FALSE + /\ pcU' = IF Fix("detach") THEN "b_clear" ELSE "b_ref" + /\ UNCHANGED <> + /\ Unchanged_S_R + +UBRefresh == \* B has no provider-side refs; viewer.setInput(B) ends with refresh() + /\ pcU = "b_ref" /\ shown' = RootSet(rootNodes) /\ view' = "B" /\ pcU' = "idle" + /\ UNCHANGED <> + /\ Unchanged_S_R + +\* ---- user: switch back to R (possibly still running) ---- +UserToR == + /\ pcU = "idle" /\ view = "B" /\ switches < MaxSwitch + /\ pcU' = "r_disp" /\ switches' = switches + 1 + /\ UNCHANGED <> + /\ Unchanged_S_R + +URDisp == + /\ pcU = "r_disp" /\ pcU' = "r_lbl" + /\ UNCHANGED <> + /\ Unchanged_S_R + +URLabel == \* RSVP:144 R.addListener(labelUpdater) + /\ pcU = "r_lbl" /\ lockL = "none" /\ pcU' = IF Fix("plock") THEN "r_add" ELSE "r_clear" + /\ UNCHANGED <> + /\ Unchanged_S_R + +URClear == \* FRSRCP:111 (fix "plock": done after addListener, under the provider lock, + \* together with the snapshot of the matches) + /\ pcU = "r_clear" /\ rootNodes' = EmptyMap /\ clears' = clears + 1 /\ provEpoch' = epoch + /\ pcU' = IF Fix("plock") THEN "r_iter" ELSE "r_add" + /\ uSnap' = IF Fix("plock") /\ Fix("snapshot") THEN matching ELSE uSnap + /\ UNCHANGED <> + /\ UNCHANGED <> + +URAdd == \* FRSRCP:116 R.addListener(this) (fix: snapshot matching under the same lock) + /\ pcU = "r_add" /\ lockL = "none" /\ provReg' = TRUE + /\ uSnap' = IF Fix("snapshot") /\ ~Fix("plock") THEN matching ELSE <<>> + /\ pcU' = IF Fix("plock") THEN "r_plk" ELSE "r_iter" + /\ UNCHANGED <> + /\ Unchanged_S_R + +URPLock == \* fix "plock": synchronized (providerLock) { clear; snapshot; addReference* } + /\ pcU = "r_plk" /\ lockP = "none" /\ lockP' = "U" /\ pcU' = "r_clear" + /\ UNCHANGED <> + /\ UNCHANGED <> + +URIter == \* FRSRCP:118 getMatchingReferences().iterator() + /\ pcU = "r_iter" /\ uCur' = 0 /\ uExp' = matchMod /\ pcU' = "r_next" + /\ UNCHANGED <> + /\ Unchanged_S_R + +URNext == \* ArrayList.Itr.hasNext (cursor != size) / next (modCount check) + /\ pcU = "r_next" + /\ LET src == IF Fix("snapshot") THEN uSnap ELSE matching IN + IF uCur = Len(src) + THEN pcU' = "r_ref" /\ UNCHANGED <> + ELSE IF ~Fix("snapshot") /\ matchMod # uExp + THEN cme' = TRUE /\ pcU' = "idle" /\ UNCHANGED <> \* CME escapes inputChanged + ELSE uRef' = src[uCur + 1] /\ uCur' = uCur + 1 /\ pcU' = "r_get" /\ UNCHANGED cme + /\ lockP' = IF pcU' # "r_get" /\ lockP = "U" THEN "none" ELSE lockP + /\ UNCHANGED <> + /\ UNCHANGED <> + +URGet == \* addReference -> resourceNode: FRSRCP:158-160 (fix "atomic") + /\ pcU = "r_get" + /\ LET u == RefUri(uRef) IN + IF rootNodes[u] # Nil + THEN uNode' = rootNodes[u] /\ pcU' = "r_child" /\ UNCHANGED <> + ELSE /\ nodes' = Append(nodes, [uri |-> u, ep |-> uRef[1], kids |-> <<>>, gen |-> clears]) + /\ uNode' = Len(nodes) + 1 + /\ IF Fix("atomic") + THEN /\ rootNodes' = [rootNodes EXCEPT ![u] = Len(nodes) + 1] + /\ batch' = Append(batch, Len(nodes) + 1) /\ pcU' = "r_child" + ELSE pcU' = "r_put" /\ UNCHANGED <> + /\ UNCHANGED <> + /\ Unchanged_S_R + +URPut == \* FRSRCP:161 + /\ pcU = "r_put" /\ rootNodes' = [rootNodes EXCEPT ![RefUri(uRef)] = uNode] /\ pcU' = "r_batch" + /\ UNCHANGED <> + /\ Unchanged_S_R + +URBatch == \* FRSRCP:162-164 + /\ pcU = "r_batch" /\ batch' = Append(batch, uNode) /\ pcU' = "r_child" + /\ UNCHANGED <> + /\ Unchanged_S_R + +URChild == \* FRSRCP:137 + /\ pcU = "r_child" /\ nodes' = AddKid(nodes, uNode, uRef) /\ pcU' = "r_next" + /\ UNCHANGED <> + /\ Unchanged_S_R + +URRefresh == \* viewer.setInput(R) -> refresh() + /\ pcU = "r_ref" /\ shown' = RootSet(rootNodes) /\ view' = "R" /\ pcU' = "idle" + /\ UNCHANGED <> + /\ Unchanged_S_R + +UIStep == UIRunSyncReset \/ UIRunAsyncReset \/ UIJobStart \/ UClear \/ UDrain \/ URefresh + \/ UCheck \/ UEnd \/ UserRerun + \/ UserToB \/ UBDisp \/ UBLabel \/ UBClear \/ UBRemove \/ UBRefresh + \/ UserToR \/ URDisp \/ URLabel \/ URClear \/ URAdd \/ URPLock \/ URIter \/ URNext + \/ URGet \/ URPut \/ URBatch \/ URChild \/ URRefresh + +Quiescent == pcS = "done" /\ pcU = "idle" /\ jobs = 0 /\ ~syncPending /\ asyncQ = <<>> + +Terminated == Quiescent /\ UNCHANGED vars \* legitimate end; anything else stuck is a deadlock + +Next == SearchStep \/ UIStep \/ Terminated + +Spec == Init /\ [][Next]_vars + +(***************************************************************************) +(* Properties *) +(***************************************************************************) +TypeOK == + /\ lockL \in {"none", "S", "U"} /\ lockP \in {"none", "S", "U"} /\ view \in {"R", "B"} /\ flag \in BOOLEAN + /\ \A u \in URIs : rootNodes[u] \in 0..Len(nodes) + /\ shown \subseteq 1..Len(nodes) + +Settled == Quiescent /\ view = "R" /\ ~cme + +RefShown(ref) == \E n \in shown : HasKid(n, ref) + +\* P1 no lost update: once quiet, every accepted reference (and its resource root) is visible +NoLostRoot == Settled => \A k \in DOMAIN matching : \E n \in shown : nodes[n].uri = RefUri(matching[k]) +NoLostRef == Settled => \A k \in DOMAIN matching : RefShown(matching[k]) + +\* P2 one root per URI (viewer, whenever the UI thread is between events) +OneRootPerUri == pcU = "idle" => \A u \in URIs : Cardinality({n \in shown : nodes[n].uri = u}) <= 1 +\* P2 at provider level: since the last rootNodes.clear() at most one root node was created per URI +OneRootCreated == \A u \in URIs : + Cardinality({n \in 1..Len(nodes) : nodes[n].uri = u /\ nodes[n].gen = clears}) <= 1 +\* P2' each reference appears once +NoDupRef == Settled => + \A n1, n2 \in shown : \A j1 \in DOMAIN nodes[n1].kids : \A j2 \in DOMAIN nodes[n2].kids : + (nodes[n1].kids[j1] = nodes[n2].kids[j2]) => (n1 = n2 /\ j1 = j2) + +\* P3 after a Reset (or re-input) no node from before it is shown, and R's nodes never leak into B +NoStale == pcU = "idle" => \A n \in shown : nodes[n].ep >= provEpoch +NoForeign == (pcU = "idle" /\ view = "B") => shown = {} + +\* Extra: no ConcurrentModificationException in inputChanged, no UI/search deadlock +NoCME == ~cme +NoDeadlock == ~(pcS = "rwait" /\ syncPending /\ lockL = "S" /\ pcU \in {"b_lbl", "b_rm", "r_lbl", "r_add"}) + +(***************************************************************************) +(* Witnesses (expected to be VIOLATED: they prove good paths are reachable) *) +(***************************************************************************) +W_AllShown == ~(Settled /\ Len(matching) = Len(Refs) /\ \A k \in DOMAIN matching : RefShown(matching[k])) +W_RerunShown == ~(Settled /\ runs = 2 /\ Len(matching) = Len(Refs) /\ \A k \in DOMAIN matching : RefShown(matching[k])) +W_SwitchBack == ~(Settled /\ switches = 2 /\ Len(matching) = Len(Refs) /\ \A k \in DOMAIN matching : RefShown(matching[k])) +W_Rescheduled == ~(pcU = "u_end" /\ uNonEmpty) +W_ResetRan == ~(provEpoch = 2 /\ pcU = "idle") +============================================================================= diff --git a/formal/find-refs/tla/FindRefsFixed.cfg b/formal/find-refs/tla/FindRefsFixed.cfg new file mode 100644 index 000000000..755ee0cc6 --- /dev/null +++ b/formal/find-refs/tla/FindRefsFixed.cfg @@ -0,0 +1,14 @@ +\* Fixed model (all minimal fixes). Must pass, including TLC deadlock checking. +SPECIFICATION Spec +CONSTANTS + Refs <- DefaultRefs + Fixes <- MinFixes + Planted = FALSE + MaxRuns = 2 + MaxSwitch = 2 +INVARIANTS + TypeOK + NoLostRoot NoLostRef + OneRootPerUri OneRootCreated NoDupRef + NoStale NoForeign + NoCME NoDeadlock diff --git a/formal/find-refs/tla/NOTES.md b/formal/find-refs/tla/NOTES.md new file mode 100644 index 000000000..4a38d359b --- /dev/null +++ b/formal/find-refs/tla/NOTES.md @@ -0,0 +1,193 @@ +# FindRefs TLA+ model: FastReferenceSearchResultContentProvider + +This directory holds a blind model of `com.avaloq.tools.ddk.xtext.ui/.../findrefs/FastReferenceSearchResultContentProvider.java` (FRSRCP). It also models the Xtext classes the provider works with: `ReferenceSearchResult` (RSR), `ReferenceQuery` and `ReferenceSearchViewPage` (RSVP), and the Eclipse Search classes `InternalSearchUI`, `SearchView` and `SearchViewManager`. The Xtext sources come from eclipse/xtext at e8855b27fd. The Eclipse Search sources come from the `org.eclipse.search.source_3.19.0` p2 bundle (extract locally; they are not committed). + +## Files +- `FindRefs.tla`: the spec, 413 non-blank lines. `Fixes` (a set of fix names) and `Planted` switch between the original code, the fixed code and the planted bug. +- `FindRefs.cfg` checks the original code. `FindRefsFixed.cfg` checks the model with all minimal fixes. +- `run.sh