I’ve made some good progress towards adding lock/unlock and rmw to herd. The C parser accepts instructions lock(l) and unlock(l). The semantics of unlock(l) is a single event structure with a single Unlock event. The semantics of lock(l) is two event structures, one with a single Lock(l,Locked) event and the other with a single Lock(l,Blocked) event. I haven’t worked out how to give the right semantics to RMW instructions yet, so for now the instruction RMW(l,v1,v2) just corresponds to a single RMW(l,v1,v2) event. More work still to be done, but at least it’s in a state where it compiles at the moment!