FlashProtocol: a TLA+ model of the FLASH cache-coherence protocol - #216

Open

lemmy wants to merge 15 commits into

tlaplus:masterfrom

lemmy:mku-flash

Commits on Jul 27, 2026

Add FlashWithMutex specification and configuration files

lemmy
and
claude
committed
FlashProtocol: refactor FlashWithMutex toward idiomatic TLA+

lemmy
and
claude
committed
Refactor FlashWithMutex specification to separate system and environment steps

lemmy
and
claude
committed
Flatten the monolithic `Sta` state record into top-level variables

lemmy
and
claude
committed
Fix NI_Local_GetX_PutX to invalidate Proc[Home] when not Dir.Local

lemmy
and
claude
committed
Encode the directory's ShrSet and InvSet as sets of nodes

lemmy
and
claude
committed
Split the multi-branch actions into disjoint guarded sub-actions

lemmy
and
claude
committed
Name the three groups of variables that share a frame condition

lemmy
and
claude
committed
Drop the write-only ghosts LastWrVld, LastWrPtr and LastInvAck

lemmy
and
claude
committed
Document the history variables

lemmy
and
claude
committed
Assign whole records where an action writes all of their fields

lemmy
and
claude
committed
Check the two-node, two-datum configuration

lemmy
and
claude
committed
Type-check and symbolically check the spec with Apalache

lemmy
and
claude
committed

Commits on Jul 28, 2026