Reasoning beyond data-race freedom

Add to your list(s) Download to your calendar using vCal

• Stephen Dolan, Ocaml Labs, University of Cambridge
• Friday 10 November 2017, 14:00-15:00
• FW26.

If you have a question about this talk, please contact Victor Gomes.

If I read a variable twice, and there are no concurrent writes to that variable, must both reads return the same value? Perhaps surprisingly, the memory models for C++ and Java do not ensure this, due to their weak guarantees in the presence of data races. These models give strong guarantees only for globally data race free programs: a data race on any variable can affect accesses to any other (C++), or to the same variable at other times (C++, Java).

In this talk, I’ll describe our work-in-progress to specify and implement a memory model for OCaml which gives useful guarantees about program behaviour even in the presence of data races, culminating in the “local DRF ” property: the data-race free parts of a program have sequential semantics, even if the rest of the program has races.

This talk is part of the Logic and Semantics Seminar (Computer Laboratory) series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Computing and Mathematics
• Department of Computer Science and Technology talks and seminars
• FW26
• Interested Talks
• Logic and Semantics Seminar (Computer Laboratory)
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31
• yk373's list

Note that ex-directory lists are not shown.