Computer Science Speaking Skills Talk

— 3:00pm

Location:
In Person - Traffic21 Classroom, Gates Hillman 6501

Speaker:
TRAVIS HANCE , Ph.D. Student, Computer Science Department, Carnegie Mellon University
https://www.andrew.cmu.edu/user/thance/

Verifying Highly-Optimized Concurrent Systems with IronSync

Concurrent software is notoriously difficult to write correctly, as programmers face the possibility of data races, potentially unintuitive memory ordering rules, or exponentially many possible thread-interleavings. Furthermore, these problems may be exacerbated in highly-tuned performant systems, where custom, low-level synchronization logic may be deeply intertwined with domain logic.  As an example of such intertwining, we consider a certain multi-threaded page cache implementation. This page cache, as part of its many optimizations, uses a single bit of a status flag both for the purposes of memory synchronization and its high-level cache logic, thus intertwining the two. In order to gain confidence in sophisticated systems like these, one solution is to produce a formally verified implementation, but this task may seem unwieldy for seemingly un-modular programs like the above. We present our verification framework, IronSync, which can handle tasks like the above. The main ingredient we employ is a linear type system, which as we will see lets us utilize efficient techniques originally developed for sequential programs in order to also handle concurrent programs. Our second ingredient is our way of structuring proofs about concurrent systems via abstract transition systems. In this talk, I will explain how the techniques work, and I will highlight key aspects of our formal verification of the page cache and their usage of the above techniques. Presented in Partial Fulfillment of the CSD Speaking Skills Requirement.


Add event to Google
Add event to iCal