Axiomatic validation of memory barriers and atomic instructions [LWN.net]

Axiomatic validation of memory barriers and atomic instructions

Posted Aug 26, 2014 8:22 UTC (Tue) by jzbiciak (guest, #5246)
In reply to: Axiomatic validation of memory barriers and atomic instructions by jzbiciak
Parent article: Axiomatic validation of memory barriers and atomic instructions

Minor clarification. On this point:

the execution time of "unconditional lock acquisition" can not be bounded

I'd like to add "... on the basis of the inputs to the lock acquisition API alone."

Basically, I was trying to capture the idea that if some code tries to take a lock unconditionally, the lock-taker's execution time is almost entirely at the mercy of the lock holder regardless of how clever the lock-taker's algorithms are. You cannot progress until the lock holder releases the lock.

And, of course, if multiple threads try to take the lock simultaneously, other threads may win ahead of this one, so the identity of "lock holder" may change during the process of attempting to acquire the lock. I don't think that changes the idea I'm attempting to express.

Stating these ideas precisely is simultaneously necessary and difficult. :-)

to post comments

Axiomatic validation of memory barriers and atomic instructions

Posted Aug 26, 2014 15:12 UTC (Tue) by PaulMcKenney (✭ supporter ✭, #9624) [Link]

Indeed, this stuff is not easy. Ten years from now, when all the details are worked out, it will probably seem a lot easier, but of course other problems will arise in the meantime. (Where would be the challenge otherwise?)

Believe it or not, in some special cases, the execution of lock acquisition can be bounded. I briefly cover this in a blog post (http://paulmck.livejournal.com/37329.html), and Bjoern Brandenburg analyzed it in depth in his dissertation (http://www.mpi-sws.org/~bbb/papers/index.html#thesis). Surprising, perhaps, but true!

Nevertheless, your original statement that lock acquisition cannot be bounded is correct in the not-uncommon case of non-FIFO locking primitives and potentially unbounded critical sections (e.g., waiting for a network packet to arrive while holding a lock). Even with FIFO locking primitives, the upper bounds for lock can grow extremely large as the number of threads increases, as the permitted lock nesting levels increase, and as the number of real-time priority levels in use increases.

Nevertheless, it is worth noting that locking does not necessarily imply unbounded execution times.