delta-io
/
delta-rs
mirror of https://github.com/delta-io/delta-rs
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity
delta-rs/tlaplus
History
QP Hou 033d690807
tla+ spec for dynamodb lock (#182) 
Spec is model checked without pause and crash.

Adding crash and pause to the modeling requires enabling timer in the
spec (i.e. setting TIME_TICK_UNIT > 0). This will fail the model check
because lock with expiration cannot guarantee correctness without use of
fencing token.
 		2021-04-13 08:55:57 -07:00
..
dynamodblock.toolbox tla+ spec for dynamodb lock (#182) 2021-04-13 08:55:57 -07:00
README.md tla+ spec for dynamodb lock (#182) 2021-04-13 08:55:57 -07:00
dynamodblock.tla tla+ spec for dynamodb lock (#182) 2021-04-13 08:55:57 -07:00

README.md

This folder contains TLA+ proofs for various subsystems of the project including:

  • Distributed Dynamodb lock
  • S3 multi-writer design

To model check these specs, you need to use TLA+ toolbox.