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).
|Features||Atomics, Locking, Witnesses|
|Path to example file||atomics/RBLock.java|
|Lines of code||117 lines (comments not included)|
|Lines of specification||53 lines (45.3% of the total)|
|Computation time||13039 milliseconds|
Note, verification may take a while and has a time-out of 20 seconds.