Example: A Concurrent Color Stack

InitColorStack() {

push(blue);

push(purple);

}

PushColor() {

if (s[top] == purple) {

ASSERT(s[top-1] == blue);

push(blue);

} else {

ASSERT(s[top] == blue);

ASSERT(s[top-1] == purple);

push(purple);

}