hengxin / tla-causal-consistency

TLA+ Specification of Variants of Causal Consistency

MIT License

6 stars 0 forks source link

TLA+ Specification of the Checking Algorithms #8

Open hengxin opened 3 years ago

hengxin commented 3 years ago

General

[x] Bad patterns
- [x] CyclicCO
- [x] WriteCOInitRead
- [x] ThinAirRead
- [x] WriteCORead
- [x] WriteHBInitRead
- [x] CyclicHB
- [x] CyclicCF
[x] Cyclic(R) in RelationUtils
[ ] Test cases
- [ ] CyclicCO
- [ ] WriteCOInitRead
- [ ] ThinAirRead
- [ ] WriteCORead
- [ ] WriteHBInitRead
- [ ] CyclicHB
- [ ] CyclicCF

CC

[x] +TLA spec
[x] +Test cases

CCv

[x] +TLA spec
[x] +Test cases

CM

[x] +TLA spec
[x] +Test cases