Skip to content

danwt/demo-percolator

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

13 Commits
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

percolator

TLA+ for Percolator.

# Check
java -XX:+UseParallelGC -Xmx12g -cp tla2tools.jar tlc2.TLC -workers auto spec.tla

This TLA+ model is of the percolator algorithm for implementing multi-row atomic transactions on top of a single-row atomic transaction system. See my blog post.

The failure model is crash stop or crash recover.

About

TLA+ for percolator.

Resources

License

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published

Languages