Tier-S: #45 Frontier 2 — concurrency / linearizability theory

[hyperpolymath]

Scope (sub-issue of #45 Frontier 2)

Concurrency / linearizability theory frontier. No proof currently states what happens with two concurrent vsh processes mutating the same filesystem.

Theorem targets

• concurrent_mkdir_safety — two concurrent mkdir p calls — exactly one succeeds, the other gets EEXIST.
• concurrent_obliterate_safety — two concurrent obliterates of the same file — at most one returns "complete proof".

Theory frontier

Herlihy-Wing linearizability for filesystem operations; per-inode locking model.

Resolution

1. Design doc (docs/THEORY-CONCURRENCY.adoc) similar to PR theory: crash-consistency design doc + Lean4 keystone theorem (crash_atomic_within_op_mkdir) #62's THEORY-CRASH-CONSISTENCY.adoc.
2. Pick a proof system (likely Lean 4 — matches CrashConsistency.lean model).
3. Add a keystone theorem to a new Concurrency.lean.
4. Practice gap: a real concurrent-vsh stress test (currently tests/stress_tests.rs doesn't fork).

References

• Parent: Filesystem-theory + practice gap analysis (POSIX 2024, atomicity, crash-consistency) #45 Frontier 2
• Companion: theory: crash-consistency design doc + Lean4 keystone theorem (crash_atomic_within_op_mkdir) #62 / Filesystem-theory + practice gap analysis (POSIX 2024, atomicity, crash-consistency) #45 Frontier 1 already addressed