Breaking and fixing Simpson's 4 slot algorithm
- 11:30 28th October 2009 ( week 3, Michaelmas Term 2009 )Room 441, Oxford University Computing Laboratory
Simpson's 4 slot algorithm is designed to turn dirty variables into a clean one. In other words, given variables in which a read concurrent with a write can produce a nondeterministic value, we want to produce a "variable" for which
- Reader and writer are not delayed
- No slot is read and written concurrently
- Every value read has recently been the most recent.
- The reads are sequentially consistent with the writes.
Simpson's algorithm uses four slots instead of the one used by the naive implementation, and four boolean flag variables. It is known to guarantee the above properties if the flag variables are themselves clean, but to have various problems if they are dirty.
I will use SVA (complete with new front end) to demonstrate this, and to develop a version which satisfies the above specifications even when all the flag variables are themselves dirty.
The complete proof of the new algorithm involves a technique for reducing an infinite-state check to a finite-state one.
Share this:
