Campus Event Calendar
Event Entry
What and Who
FSL: A Program Logic for C11 Memory Fences
Marko Doko
MMCI
SWS Student Defense Talks - Qualifying Exam
SWS
Expert Audience
English
Note: We use this to send email in the morning.
Date, Time and Location
Friday, 16 October 2015
13:00
60 Minutes
G26
111
Kaiserslautern
Abstract
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.
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.
Contact
--email hidden
passcode not visible
logged in users only
Maria-Louise Albrecht, 03/11/2016 11:02 -- Created document.