BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Programming and Proving with Fine-Grained Concurrent Resources - I
 lya Sergey\, IMDEA Software Institute
DTSTART:20150305T100000Z
DTEND:20150305T110000Z
UID:TALK58217@talks.cam.ac.uk
CONTACT:Microsoft Research Cambridge Talks Admins
DESCRIPTION:In the past decade\, significant progress has been made toward
 s design and development of efficient fine-grained (i.e.\, lock-free) conc
 urrent data structures and algorithms\, which take full advantage of paral
 lel computations. Due to sophisticated interference scenarios and a large 
 number of possible interactions between concurrent threads\, working over 
 the same shared data structures and employing fine-grained synchronization
  primitives (e.g.\, compare-and-swap command)\, ensuring correctness of fi
 ne-grained concurrent programs is challenging and error-prone.\n\nIn my ta
 lk\, through a series of examples\, I will introduce Fine-grained Concurre
 nt Separation Logic (FCSL) - a mechanized logical  framework for implement
 ing and verifying fine-grained  concurrent programs.\n\nFCSL models effect
 s of concurrent threads\, manipulating shared resources\, via two basic ma
 thematical structures: state-transition systems (STSs) and partial commuta
 tive monoids (PCMs). Being simple enough\, this model of concurrent resour
 ces\, in combination with a small number of program and proof-level comman
 ds\, is sufficient to give useful specifications and verify a large class 
 of state-of-the-art concurrent libraries. By employing expressive type the
 ory as a way to ascribe specifications to effectful programs\, FCSL achiev
 es scalability: even though the proofs for libraries might be large\, they
  are done just once.\n\nFCSL was proved sound with respect to the denotati
 onal semantic of action trees and implemented as a monadic embedding in Co
 q\, a general-purpose mechanized framework for formal proofs. That is\, co
 ncurrent programs written in FCSL’s language are also Coq programs\, so 
 they can make use of all Coq’s features as a programming language.\nAs a
  part of my talk\, I will demonstrate how proofs about concurrent programs
  in FCSL can be done directly in Coq\, taking advantage of Coq’s interac
 tive proof construction machinery.\n
LOCATION:Auditorium\, Microsoft Research Ltd\, 21 Station Road\, Cambridge
 \, CB1 2FB
END:VEVENT
END:VCALENDAR