This project is read-only.

vcc(atomic_inline)

The CPU usually supports a number of atomic memory operations beside reading and writing. One example is _InterlockedCompareAndExchange(p, n, o), which atomically checks if *p == o and if so stores n at *p. In any event it returns the old value of *p. Because the set of such operations vary from machine to machine, VCC supports the notion of atomic_inline functions, for example the _InterlockedCompareAndExchange(...) can be specified as follows:

#include <vcc.h>

vcc(atomic_inline)
long _InterlockedCompareExchange(volatile long *Destination, long Exchange, long Comparand)
#ifdef VERIFY
{
    if (*Destination == Comparand) {
        *Destination = Exchange;
        return Comparand;
    } else {
        return *Destination;
    }
}
#endif
;


It's up to the person implementing the atomic inline functions to make sure the underlying machine primitive does what the body of the function said it does.

A atomic inline function call can be only used inside of an atomic block and counts as a single physical update. In other words you can only call one of these in an atomic block, and once you call them, you cannot perform any other atomic read or write.

Last edited Nov 13, 2009 at 1:02 PM by stobies, version 3

Comments

No comments yet.