BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:A Program Logic for Concurrent Objects under Fair Scheduling - Hon
 gjin Liang\, USTC
DTSTART:20150910T133000Z
DTEND:20150910T143000Z
UID:TALK60580@talks.cam.ac.uk
CONTACT:Microsoft Research Cambridge Talks Admins
DESCRIPTION:Existing work on verifying concurrent objects is mostly concer
 ned with safety only\, e.g.\, partial correctness or linearizability. Alth
 ough there has been recent work verifying lock-freedom of non-blocking obj
 ects\, much less efforts are focused on deadlock-freedom and starvation-fr
 eedom\, progress properties of blocking objects. These properties are more
  challenging to verify than lock-freedom because they allow the progress o
 f one thread to depend on the progress of another\, assuming fair scheduli
 ng.\n\nWe propose LiLi\, a new rely-guarantee style program logic for veri
 fying linearizability and progress together for concurrent objects under f
 air scheduling. The rely-guarantee style logic unifies thread-modular reas
 oning about both starvation-freedom and deadlock-freedom in one framework.
  It also establishes progress-aware abstraction for concurrent objects\, w
 hich can be applied when verifying safety and liveness of client code. We 
 have successfully applied the logic to verify starvation-freedom or deadlo
 ck-freedom of representative algorithms such as ticket locks\, queue locks
 \, lock-coupling lists\, optimistic lists and lazy lists.\n
LOCATION:Small lecture room\, Microsoft Research Ltd\, 21 Station Road\, C
 ambridge\, CB1 2FB
END:VEVENT
END:VCALENDAR