New Operating Systems Review Issue

The latest issue of ACM OSR (vol. 54, no. 1) is now available in the ACM Digital Library. With seven papers, this issue addresses the special topics: formal methods and verification; and synchronization and locking Mechanisms.

Formal Methods and Verification

Towards Provable Timing-Channel Prevention. By Gernot Heiser, Toby Murray, and Gerwin Klein (UNSW, Sydney).

überSpark: Practical, Provable, End-to-End Guarantees on Commodity Heterogenous Interconnected Computing Platforms. By Amit Vasudevan, Petros Maniatis, and Ruben Martins (Carnegie Mellon University and Google Research).

Simple High-Level Code For Cryptographic Arithmetic: With Proofs, Without Compromises. By Andres Erbsen, Jade Philipoom, Jason Gross, Robert Sloan, and Adam Chlipala (MIT CSAIL).

Noninterference specifications for secure systems. By Luke Nelson, James Bornholt, Arvind Krishnamurthy, Emina Torlak, and Xi Wang (University of Washington and UT Austin)

Verifiable state machines: Proofs that untrusted services operate correctly. By Srinath Setty, Sebastian Angel, and Jonathan Lee (Microsoft Research and University of Pennsylvania)

Synchronization and Locking Mechanisms

RCU Usage In the Linux Kernel: Eighteen Years Later. By Paul E. McKenney, Joel Fernandes, Silas Boyd-Wickizer, and Jonathan Walpole (Facebook, Google, MIT CSAIL, and Portland State University)

Symbolic Reasoning for Automatic Signal Placement. ByKostas Ferles, Jacob Van Geffen, Isil Dillig, and Yannis Smaragdakis (UT Austin and University of Athens)


We would like to thank the editors Robbert van Renesse, Christopher J. Rossbach, Kishore Pusukuri, John Chandy, Antônio Fröhlich, and Ashvin Goel for their efforts on this issue.