Types and Safety of Lock-free Data Structures

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

• Elias Castegren, MSR
• Friday 29 June 2018, 14:00-15:00
• FW26.

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

The increasing importance of parallel and concurrent programming has rejuvenated interest in systems that statically control the use of shared mutable state in order to guarantee properties such as data-race freedom. This control is commonly achieved by banning concurrent access to mutable state altogether, either through isolation (e.g., ownership types), synchronisation (e.g., by enforcing correct usage of locks), immutability (e.g., read-only references), or uniqueness (e.g., linear references).

Banning shared mutable state simplifies reasoning about concurrent programs—for programmers as well as for optimizing compilers – but it is too strong a restriction for many applications. Notably, lock-free algorithms, which implement protocols that ensure safe, non-blocking concurrent access to data structures, generally rely on shared mutable state to achieve lock-freedom.

This presentation details the work on LOLCAT , a type system that allows an unbounded number of aliases to a shared mutable resource, as long as at most one alias at a time owns the right to access the contents of the resource. This ownership can be transferred between aliases, but can never be duplicated. LOLCAT types are flexible enough to type several lock-free data structures, but also powerful enough to give a compile-time guarantee of absence of data-races when accessing owned data. In particular, LOLCAT is able to assign meaningful types to the CAS (compare and swap) primitive that precisely describe how ownership is transferred across aliases, possibly across different threads.

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.