Single-entrant spin lock

SESLock is the single-entrant spin lock using an AtomicInteger as synchroniser. The contracts for the AtomicInteger is the version without magic-wand (delta).

General information

ID19
Articlenone
Back-endChalice
LanguageJava
FeaturesAtomics, Locking, Witnesses
Sources
Path to example fileatomics/RBLock.java
Date2017-06-15

Statistical information

Lines of code117 lines (comments not included)
Lines of specification53 lines (45.3% of the total)
Computation time13039 milliseconds

Example code

Note, verification may take a while and has a time-out of 20 seconds.