Fenced Separation Logic

Fenced separation logic (FSL) is a program logic for reasoning about concurrent programs under the C11 memory model. FSL is an extension of relaxed separation logic (RSL) with added support for reasoning about memory fences. Specifically, it extends RSL with two modalidities for describing state that is protected by fences (either by a previous release fence or by a later acquire fence).



Other relaxed program logics