Demonstrates a bug that was fixed in aiorwlock.
aiorwlock_bug.tla and aiorwlock.tla represent the lock before and after the fix. aiorwlock.tla was only changed slightly from the original spec.
- Original spec: https://github.com/aio-libs/aiorwlock/blob/853b736/spec/aiorwlock.tla
- Talk (in Russian): https://www.youtube.com/watch?v=gRr9ymtAN6E
- Slides (in English): https://www.slideshare.net/MykolaNovik/verification-of-concurrent-and-distributed-systems