Follow-up to PR #62 (crash-consistency keystone). See docs/THEORY-CRASH-CONSISTENCY.adoc § Frontier A.
Statement
The keystone says nothing about two concurrent vsh processes, or vsh + external editor, or vsh in a container with sibling processes on the same mount. The current Lean 4 model is purely sequential.
Proposed approach
Herlihy-Wing-style linearizability. Each FilesystemOp gets a linearization point (journal-commit on ext4, COW commit on ZFS). For every interleaving of two processes' operations there exists a sequential schedule producing the same observable history. First tractable slice: 'non-overlapping-path operations linearize trivially under per-path locks' (matches PROOF-OPEN-FRONTIER.adoc#F-4).
Interaction with keystone
Concurrent crash = crash + non-trivial schedule. Linearizability layers on top of atomicity-within-op, not in place of it.
Gates
Need to choose a concurrency framework. Iris in Coq is one option; native Lean 4 Concurrent reasoning is another.
Tier: S (Foundational gap).
Follow-up to PR #62 (crash-consistency keystone). See
docs/THEORY-CRASH-CONSISTENCY.adoc§ Frontier A.Statement
The keystone says nothing about two concurrent vsh processes, or vsh + external editor, or vsh in a container with sibling processes on the same mount. The current Lean 4 model is purely sequential.
Proposed approach
Herlihy-Wing-style linearizability. Each
FilesystemOpgets a linearization point (journal-commit on ext4, COW commit on ZFS). For every interleaving of two processes' operations there exists a sequential schedule producing the same observable history. First tractable slice: 'non-overlapping-path operations linearize trivially under per-path locks' (matchesPROOF-OPEN-FRONTIER.adoc#F-4).Interaction with keystone
Concurrent crash = crash + non-trivial schedule. Linearizability layers on top of atomicity-within-op, not in place of it.
Gates
Need to choose a concurrency framework. Iris in Coq is one option; native Lean 4
Concurrentreasoning is another.Tier: S (Foundational gap).