weak memory C11 programs in the Event-B framework.
We build on a recently developed operational semantics for
the RAR fragment of C11, which we use as a top-level abstraction.
In our technique, a concrete C11 program can be
modelled by refining this abstract model of the semantics.
Program structures and individual operations are then introduced
in the refined machine and can be checked and
verified using available Event-B provers and model checkers.
The paper also discusses how ProB model checker can be
used to validate the Event-B model of C11 programs. We applied
our technique to the C11 implementation of Peterson?s
algorithm, where we discovered that the standard invariant
used to characterise mutual exclusion is inadaquate. We
therefore propose and verify new invariants necessary for
characterising mutual exclusion in a weak memory setting.