Axiomatic validation of memory barriers and atomic instructions

Axiomatic validation of memory barriers and atomic instructions

I think I missed that article the first time 'round. Thank you for linking it.

FWIW, on "future work" item #3, it seems like unconditional lock acquisition is equivalent to either:

• A function with a return value that says that you acquired the lock (and just always happens to be 'true'), or
• A function with a while-loop around a call to a conditional lock acquisition function that spins until the lock is actually acquired.

Those two statements actually say the same thing under the hood—that there's a fundamental step with a return value (whether you acquired the lock) and a composite step that repeats the fundamental step until a goal is achieved (you actually acquired the lock).

To tease this apart in the SNC framework, it seems like you need some additional criterion to determine whether your measurement point for SNC-ness is at the appropriate level, or that you must drill down.

In this case, the execution time of "unconditional lock acquisition" can not be bounded because it depends on the state of the lock and the behavior of the other lock holders, and so represents SNC communication. (In this case, to the CPU's conditional branch circuitry.) That suggests a potential criterion stated in terms of the termination condition for the API. If the termination condition that allows the API to exit is SNC, the API is SNC.

At least, that's my initial gut feel after reading that article.