In this talk, we'll describe a simple, but powerful, program logic for reasoning
about C11 relaxed accesses used in conjunction with release and
acquire memory fences. Our logic, called fenced separation logic (FSL),
extends relaxed separation logic with special modalities for describing
state that has to be protected by memory fences. Like its precursor, FSL
allows ownership transfer over synchronizations and can be used to verify
the message-passing idiom and other similar programs. The soundness
of FSL has been established in Coq.