More Web Proxy on the site http://driver.im/

research-article

Using concurrent relational logic with helpers for verifying the AtomFS file system

Authors:

Haibo ChenAuthors Info & Claims

SOSP '19: Proceedings of the 27th ACM Symposium on Operating Systems Principles

Pages 259 - 274

https://doi.org/10.1145/3341301.3359644

Published: 27 October 2019 Publication History

Abstract

Concurrent file systems are pervasive but hard to correctly implement and formally verify due to nondeterministic interleavings. This paper presents AtomFS, the first formally-verified, fine-grained, concurrent file system, which provides linearizable interfaces to applications. The standard way to prove linearizability requires modeling linearization point of each operation---the moment when its effect becomes visible atomically to other threads. We observe that path inter-dependency, where one operation (like rename) breaks the path integrity of other operations, makes the linearization point external and thus poses a significant challenge to prove linearizability.

To overcome the above challenge, this paper presents <u>C</u>oncurrent <u>R</u>elational <u>L</u>ogic with <u>H</u>elpers (CRL-H), a framework for building verified concurrent file systems. CRL-H is made powerful through two key contributions: (1) extending prior approaches using fixed linearization points with a helper mechanism where one operation of the thread can logically help other threads linearize their operations; (2) combining relational specifications and rely/guarantee conditions for relational and compositional reasoning. We have successfully applied CRL-H to verify the linearizability of AtomFS directly in C code. All the proofs are mechanized in Coq. Evaluations show that AtomFS speeds up file system workloads by utilizing fine-grained, multicore concurrency.

References

[1]

2019. FreeBSD Handbook. https://www.freebsd.org/doc/handbook/ Referenced April 2019.

[2]

2019. Reiser4 FS Wiki. https://reiser4.wiki.kernel.org/index.php/Main_Page Referenced April 2019.

[3]

2019. tmpfs - Linux manual page. http://man7.org/linux/man-pages/man5/tmpfs.5.html Referenced April 2019.

[4]

2019. Toward better testing. https://lwn.net/Articles/591985/ Referenced August 2019.

[5]

Sidney Amani, Alex Hixon, Zilin Chen, Christine Rizkallah, Peter Chubb, Liam O'Connor, Joel Beeren, Yutaka Nagashima, Japheth Lim, Thomas Sewell, Joseph Tuong, Gabriele Keller, Toby Murray, Gerwin Klein, and Gernot Heiser. 2016. Cogent: Verifying High-Assurance File System Implementations. In Proceedings of the Twenty-First International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS '16). ACM, New York, NY, USA, 175--188.

Digital Library

[6]

Srivatsa S Bhat, Rasha Eqbal, Austin T Clements, M Frans Kaashoek, and Nickolai Zeldovich. 2017. Scaling a file system to many cores using an operation log. In Proceedings of the 26th Symposium on Operating Systems Principles. ACM, 69--86.

Digital Library

[7]

Jeff Bonwick and Bill Moore. 2007. ZFS: The last word in file systems.

[8]

Stephen Brookes. 2007. A semantics for concurrent separation logic. Theoretical Computer Science 375, 1--3 (2007), 227--270.

Digital Library

[9]

Miao Cai, Hao Huang, and Jian Huang. 2019. Understanding Security Vulnerabilities in File Systems. In Proceedings of the 10th ACM SIGOPS Asia-Pacific Workshop on Systems (APSys '19). ACM, New York, NY, USA, 8--15.

Digital Library

[10]

Remy Card. 1995. Design and implementation of the second extended filesystem. In Proceedings of the First Dutch International Symposium on Linux, 1995.

[11]

Tej Chajed. 2017. Verifying an i/o-concurrent file system. Master's thesis. Massachusetts Institute of Technology.

[12]

Tej Chajed, Frans Kaashoek, Butler Lampson, and Nickolai Zeldovich. 2018. Verifying concurrent software using movers in {CSPEC}. In 13th {USENIX} Symposium on Operating Systems Design and Implementation ({OSDI} 18). 306--322.

[13]

Tej Chajed, Joseph Tassarotti, M. Frans Kaashoek, and Nickolai Zeldovich. 2019. Verifying concurrent, crash-safe systems with Perennial. In Proceedings of the 27th ACM Symposium on Operating Systems Principles (SOSP 2019). Huntsville, Ontario, Canada.

Digital Library

[14]

Haogang Chen, Tej Chajed, Alex Konradi, Stephanie Wang, Atalay İleri, Adam Chlipala, M Frans Kaashoek, and Nickolai Zeldovich. 2017. Verifying a high-performance crash-safe file system using a tree specification. In Proceedings of the 26th Symposium on Operating Systems Principles. ACM, 270--286.

Digital Library

[15]

Hao Chen, Xiongnan Newman Wu, Zhong Shao, Joshua Lockerman, and Ronghui Gu. 2016. Toward compositional verification of interruptible OS kernels and device drivers. In ACM SIGPLAN Notices, Vol. 51. ACM, 431--447.

Digital Library

[16]

Haogang Chen, Daniel Ziegler, Tej Chajed, Adam Chlipala, M Frans Kaashoek, and Nickolai Zeldovich. 2015. Using Crash Hoare logic for certifying the FSCQ file system. In Proceedings of the 25th Symposium on Operating Systems Principles. ACM, 18--37.

Digital Library

[17]

Ernie Cohen, Markus Dahlweid, Mark Hillebrand, Dirk Leinenbach, Michał Moskal, Thomas Santen, Wolfram Schulte, and Stephan Tobies. 2009. VCC: A practical system for verifying concurrent C. In International Conference on Theorem Proving in Higher Order Logics. Springer, 23--42.

Digital Library

[18]

Robert Colvin, Lindsay Groves, Victor Luchangco, and Mark Moir. 2006. Formal verification of a lazy concurrent list-based set algorithm. In International Conference on Computer Aided Verification. Springer, 475--488.

Digital Library

[19]

Russ Cox, M Frans Kaashoek, and Robert Morris. 2011. Xv6, a simple Unix-like teaching operating system.

[20]

W-P De Roever, Frank de Boer, Ulrich Hanneman, Jozef Hooman, Yassine Lakhnech, Mannes Poel, and Job Zwiers. 2001. Concurrency verification: Introduction to compositional and non-compositional methods. Vol. 54. Cambridge University Press.

[21]

Willem-Paul De Roever, Kai Engelhardt, and Karl-Heinz Buth. 1998. Data refinement: model-oriented proof methods and their comparison. Vol. 47. Cambridge University Press.

[22]

John Derrick, Gerhard Schellhorn, and Heike Wehrheim. 2011. Mechanically verified proof obligations for linearizability. ACM Transactions on Programming Languages and Systems (TOPLAS) 33, 1 (2011), 4.

Digital Library

[23]

John Derrick, Gerhard Schellhorn, and Heike Wehrheim. 2011. Verifying linearisability with potential linearisation points. In International Symposium on Formal Methods. Springer, 323--337.

[24]

Coq development team. 2019. The Coq Proof Assistant. http://coq.inria.fr/

[25]

Brijesh Dongol and John Derrick. 2015. Verifying linearisability: A comparative survey. ACM Computing Surveys (CSUR) 48, 2 (2015), 19.

Digital Library

[26]

Cezara Drąoi, Ashutosh Gupta, and Thomas A Henzinger. 2013. Automatic linearizability proofs of concurrent objects with cooperating updates. In International Conference on Computer Aided Verification. Springer, 174--190.

[27]

Xinyu Feng. 2009. Local rely-guarantee reasoning. In ACM SIGPLAN Notices, Vol. 44. ACM, 315--327.

Digital Library

[28]

Xinyu Feng, Rodrigo Ferreira, and Zhong Shao. 2007. On the relationship between concurrent separation logic and assume-guarantee reasoning. In European Symposium on Programming. Springer, 173--188.

[29]

Filebench. 2019. Filebench. https://github.com/filebench/filebench

[30]

Ivana Filipović, Peter OHearn, Noam Rinetzky, and Hongseok Yang. 2010. Abstraction for concurrent objects. Theoretical Computer Science 411, 51--52 (2010), 4379--4398.

Digital Library

[31]

Dan Frumin, Robbert Krebbers, and Lars Birkedal. 2018. ReLoC: A mechanised relational logic for fine-grained concurrency. In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science. ACM, 442--451.

Digital Library

[32]

FUSE. 2019. The reference implementation of the Linux FUSE (Filesystem in Userspace) interface. https://github.com/libfuse/libfuse

[33]

GNU. 2019. GCC, the GNU Compiler Collection. https://www.gnu.org/software/gcc/. Referenced April 2019.

[34]

Ronghui Gu, Zhong Shao, Hao Chen, Xiongnan (Newman) Wu, Jieung Kim, Vilhelm Sjöberg, and David Costanzo. 2016. CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels. In 12th USENIX Symposium on Operating Systems Design and Implementation (OSDI 16). USENIX Association, Savannah, GA, 653--669. https://www.usenix.org/conference/osdi16/technical-sessions/presentation/gu

Digital Library

[35]

Ronghui Gu, Zhong Shao, Jieung Kim, Xiongnan Newman Wu, Jérémie Koenig, Vilhelm Sjöberg, Hao Chen, David Costanzo, and Tahina Ramananandro. 2018. Certified concurrent abstraction layers. In Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation. ACM, 646--661.

Digital Library

[36]

Chris Hawblitzel, Erez Petrank, Shaz Qadeer, and Serdar Tasiran. 2015. Automated and modular refinement reasoning for concurrent programs. In International Conference on Computer Aided Verification. Springer, 449--465.

[37]

Danny Hendler, Nir Shavit, and Lena Yerushalmi. 2004. A scalable lock-free stack algorithm. In Proceedings of the sixteenth annual ACM symposium on Parallelism in algorithms and architectures. ACM, 206--215.

Digital Library

[38]

Maurice Herlihy and Nir Shavit. 2011. The art of multiprocessor programming. Morgan Kaufmann.

[39]

Maurice P Herlihy and Jeannette M Wing. 1990. Linearizability: A correctness condition for concurrent objects. ACM Transactions on Programming Languages and Systems (TOPLAS) 12, 3 (1990), 463--492.

Digital Library

[40]

Charles Antony Richard Hoare. 1969. An axiomatic basis for computer programming. Commun. ACM 12, 10 (1969), 576--580.

Digital Library

[41]

Atalay Ileri, Tej Chajed, Adam Chlipala, Frans Kaashoek, and Nickolai Zeldovich. 2018. Proving confidentiality in a file system using DiskSec. In 13th USENIX Symposium on Operating Systems Design and Implementation (OSDI 18). USENIX Association, Carlsbad, CA, 323--338. https://www.usenix.org/conference/osdi18/presentation/ileri

[42]

Cliff B. Jones. 1983. Tentative steps toward a development method for interfering programs. ACM Transactions on Programming Languages and Systems (TOPLAS) 5, 4 (1983), 596--619.

Digital Library

[43]

D. Jones. 2019. Trinity: A Linux system call fuzz tester. http://codemonkey.org.uk/projects/trinity/

[44]

Artem Khyzha, Mike Dodds, Alexey Gotsman, and Matthew Parkinson. 2017. Proving linearizability using partial orders. In European Symposium on Programming. Springer, 639--667.

Digital Library

[45]

Jieung Kim, Vilhelm Sjöberg, Ronghui Gu, and Zhong Shao. 2017. Safety and Liveness of MCS Lock---Layer by Layer. In Asian Symposium on Programming Languages and Systems. Springer, 273--297.

[46]

Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, et al. 2009. seL4: Formal verification of an OS kernel. In Proceedings of the ACM SIGOPS 22nd symposium on Operating systems principles. ACM, 207--220.

Digital Library

[47]

Mohsen Lesani, Christian J Bell, and Adam Chlipala. 2016. Chapar: certified causally consistent distributed key-value stores. In ACM SIGPLAN Notices, Vol. 51. ACM, 357--370.

Digital Library

[48]

Hongjin Liang and Xinyu Feng. 2013. Modular verification of linearizability with non-fixed linearization points. In ACM SIGPLAN Notices, Vol. 48. ACM, 459--470.

Digital Library

[49]

Hongjin Liang, Xinyu Feng, and Ming Fu. 2012. A rely-guarantee-based simulation for verifying concurrent program transformations. In ACM SIGPLAN Notices, Vol. 47. ACM, 455--468.

Digital Library

[50]

Hongjin Liang, Xinyu Feng, and Zhong Shao. 2014. Compositional verification of termination-preserving refinement of concurrent programs. In Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). ACM, 65.

Digital Library

[51]

Linux. 2019. Pathname lookup; The Linux Kernel documentation. https://www.kernel.org/doc/html/latest/filesystems/path-lookup.html. Referenced April 2019.

[52]

Richard J Lipton. 1975. Reduction: A method of proving properties of parallel programs. Commun. ACM 18, 12 (1975), 717--721.

Digital Library

[53]

Lanyue Lu, Andrea C Arpaci-Dusseau, Remzi H Arpaci-Dusseau, and Shan Lu. 2013. A study of Linux file system evolution. In Presented as part of the 11th {USENIX} Conference on File and Storage Technologies ({FAST} 13). 31--44.

[54]

Nancy Lynch and Frits Vaandrager. 1995. Forward and backward simulations. Information and Computation 121, 2 (1995), 214--233.

Digital Library

[55]

Chris Mason. 2007. The btrfs filesystem. The Orcale cooperation (2007).

[56]

Changwoo Min, Sanidhya Kashyap, Byoungyoung Lee, Chengyu Song, and Taesoo Kim. 2015. Cross-checking semantic correctness: The case of finding file system bugs. In Proceedings of the 25th Symposium on Operating Systems Principles. ACM, 361--377.

Digital Library

[57]

mit pdos. 2019. mit-pdos/fscq: FSCQ is a certified file system written and proven in Coq. https://github.com/mit-pdos/fscq. Referenced April 2019.

[58]

Ben C Moszkowski. 1997. Compositional reasoning using interval temporal logic and tempura. In International Symposium on Compositionality. Springer, 439--464.

[59]

Gian Ntzik. 2016. Reasoning about POSIX file systems. Ph.D. Dissertation. Imperial College London.

[60]

Gian Ntzik, Pedro da Rocha Pinto, Julian Sutherland, and Philippa Gardner. 2018. A concurrent specification of POSIX file systems. In 32nd European Conference on Object-Oriented Programming (ECOOP 2018). Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik.

[61]

Susan Owicki and David Gries. 1976. Verifying properties of parallel programs: An axiomatic approach. Commun. ACM 19, 5 (1976), 279--285.

Digital Library

[62]

Peter O'Hearn, John Reynolds, and Hongseok Yang. 2001. Local reasoning about programs that alter data structures. In International Workshop on Computer Science Logic. Springer, 1--19.

[63]

Thanumalayan Sankaranarayana Pillai, Vijay Chidambaram, Ramnatthan Alagappan, Samer Al-Kiswany, Andrea C Arpaci-Dusseau, and Remzi H Arpaci-Dusseau. 2014. All file systems are not created equal: On the complexity of crafting crash-consistent applications. In 11th {USENIX} Symposium on Operating Systems Design and Implementation ({OSDI} 14). 433--448.

[64]

John C Reynolds. 2002. Separation logic: A logic for shared mutable data structures. In Proceedings 17th Annual IEEE Symposium on Logic in Computer Science. IEEE, 55--74.

[65]

Mendel Rosenblum and John K Ousterhout. 1991. The design and implementation of a log-structured file system. In ACM SIGOPS Operating Systems Review, Vol. 25. ACM, 1--15.

Digital Library

[66]

Helgi Sigurbjarnarson, James Bornholt, Emina Torlak, and Xi Wang. 2016. Push-Button Verification of File Systems via Crash Refinement. In 12th USENIX Symposium on Operating Systems Design and Implementation (OSDI 16). USENIX Association, Savannah, GA, 1--16. https://www.usenix.org/conference/osdi16/technical-sessions/presentation/sigurbjarnarson

[67]

Kuei Sun, Matthew Lakier, Angela Demke Brown, and Ashvin Goel. 2018. Breaking Apart the {VFS} for Managing File Systems. In 10th {USENIX} Workshop on Hot Topics in Storage and File Systems (Hot-Storage 18).

[68]

Adam Sweeney, Doug Doucette, Wei Hu, Curtis Anderson, Mike Nishimoto, and Geoff Peck. 1996. Scalability in the XFS File System. In USENIX Annual Technical Conference, Vol. 15.

Digital Library

[69]

Theodore Ts'o and Stephen Tweedie. 2002. Future directions for the ext2/3 filesystem. In Proceedings of the USENIX annual technical conference (FREENIX track).

[70]

Aaron J Turon, Jacob Thamsborg, Amal Ahmed, Lars Birkedal, and Derek Dreyer. 2013. Logical relations for fine-grained concurrency. In ACM SIGPLAN Notices, Vol. 48. ACM, 343--356.

Digital Library

[71]

Viktor Vafeiadis. 2008. Modular fine-grained concurrency verification. Technical Report. University of Cambridge, Computer Laboratory.

[72]

Viktor Vafeiadis. 2011. Concurrent separation logic and operational semantics. Electronic Notes in Theoretical Computer Science 276 (2011), 335--351.

Digital Library

[73]

Viktor Vafeiadis and Matthew Parkinson. 2007. A marriage of rely/guarantee and separation logic. In International Conference on Concurrency Theory. Springer, 256--271.

[74]

vim. 2019. welcome home: vim online. https://www.vim.org. Referenced April 2019.

[75]

James R Wilcox, Doug Woos, Pavel Panchekha, Zachary Tatlock, Xi Wang, Michael D Ernst, and Thomas Anderson. 2015. Verdi: a framework for implementing and formally verifying distributed systems. In ACM SIGPLAN Notices, Vol. 50. ACM, 357--368.

Digital Library

[76]

Fengwei Xu, Ming Fu, Xinyu Feng, Xiaoran Zhang, Hui Zhang, and Zhaohui Li. 2016. A practical verification framework for preemptive OS kernels. In International Conference on Computer Aided Verification. Springer, 59--79.

[77]

Junfeng Yang, Paul Twohey, Dawson Engler, and Madanlal Musuvathi. 2006. Using model checking to find serious file system errors. ACM Transactions on Computer Systems (TOCS) 24, 4 (2006), 393--423.

Digital Library

Cited By

Liu YAdkar MHolzmann GKuenning GLiu PSmolka SSu WZadok EMa XWon Y(2024)MetisProceedings of the 22nd USENIX Conference on File and Storage Technologies10.5555/3650697.3650705(123-140)Online publication date: 27-Feb-2024
https://dl.acm.org/doi/10.5555/3650697.3650705
Liu JHao XArpaci-Dusseau AArpaci-Dusseau RChajed T(2024)Shadow Filesystems: Recovering from Filesystem Runtime Errors via Robust Alternative ExecutionProceedings of the 16th ACM Workshop on Hot Topics in Storage and File Systems10.1145/3655038.3665942(15-22)Online publication date: 8-Jul-2024
https://dl.acm.org/doi/10.1145/3655038.3665942
Zhuo DZhang KLi ZZhuang SWang SChen AStoica I(2022)Rearchitecting in-memory object stores for low latencyProceedings of the VLDB Endowment10.14778/3494124.349413815:3(555-568)Online publication date: 4-Feb-2022
https://dl.acm.org/doi/10.14778/3494124.3494138
Show More Cited By

Recommendations

Concurrent file metadata structure using readers-writer lock
SAC '21: Proceedings of the 36th Annual ACM Symposium on Applied Computing

Linux file systems serialize threads when writing shared files. Recent studies have attempted to adopt range locks on shared files to solve this serialization problem, allowing file I/O to be executed concurrently. However, we have found that even with ...
Verifying concurrent programs: tutorial talk
FMCAD '11: Proceedings of the International Conference on Formal Methods in Computer-Aided Design

The proliferation of multi-core hardware has led to widespread use of concurrent programs. However, these programs are notoriously difficult to get right and to debug for developers. Even for automated verification, it is a big challenge to reason about ...
Verifying concurrent probabilistic systems using probabilistic-epistemic logic specifications

In this paper, we address the problem of verifying probabilistic and epistemic properties in concurrent probabilistic systems expressed in PCTLK. PCTLK is an extension of the Probabilistic Computation Tree Logic (PCTL) augmented with Knowledge (K). In ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

SOSP '19: Proceedings of the 27th ACM Symposium on Operating Systems Principles

October 2019

615 pages

ISBN:9781450368735

DOI:10.1145/3341301

General Chairs:
Tim Brecht
University of Waterloo
,
Carey Williamson
University of Calgary

Copyright © 2019 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].

Sponsors

SIGOPS: ACM Special Interest Group on Operating Systems

In-Cooperation

USENIX Assoc: USENIX Assoc

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 27 October 2019

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Research-article

Conference

SOSP '19

Sponsor:

SIGOPS

SOSP '19: ACM SIGOPS 27th Symposium on Operating Systems Principles

October 27 - 30, 2019

Ontario, Huntsville, Canada

Acceptance Rates

Overall Acceptance Rate 174 of 961 submissions, 18%

Upcoming Conference

SOSP '25

Sponsor:
sigops

ACM SIGOPS 31st Symposium on Operating Systems Principles

October 13 - 16, 2025

Seoul , Republic of Korea

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

13
Total Citations
View Citations
950
Total Downloads

Downloads (Last 12 months)70
Downloads (Last 6 weeks)8

Reflects downloads up to 30 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Liu YAdkar MHolzmann GKuenning GLiu PSmolka SSu WZadok EMa XWon Y(2024)MetisProceedings of the 22nd USENIX Conference on File and Storage Technologies10.5555/3650697.3650705(123-140)Online publication date: 27-Feb-2024
https://dl.acm.org/doi/10.5555/3650697.3650705
Liu JHao XArpaci-Dusseau AArpaci-Dusseau RChajed T(2024)Shadow Filesystems: Recovering from Filesystem Runtime Errors via Robust Alternative ExecutionProceedings of the 16th ACM Workshop on Hot Topics in Storage and File Systems10.1145/3655038.3665942(15-22)Online publication date: 8-Jul-2024
https://dl.acm.org/doi/10.1145/3655038.3665942
Zhuo DZhang KLi ZZhuang SWang SChen AStoica I(2022)Rearchitecting in-memory object stores for low latencyProceedings of the VLDB Endowment10.14778/3494124.349413815:3(555-568)Online publication date: 4-Feb-2022
https://dl.acm.org/doi/10.14778/3494124.3494138
Bodenmüller SSchellhorn GReif W(2022)Verification of Crashsafe Caching in a Virtual File System SwitchFormal Aspects of Computing10.1145/352373734:1(1-33)Online publication date: 5-Jul-2022
https://dl.acm.org/doi/10.1145/3523737
Vindum SFrumin DBirkedal LPopescu AZdancewic S(2022)Mechanized verification of a fine-grained concurrent queue from meta’s folly libraryProceedings of the 11th ACM SIGPLAN International Conference on Certified Programs and Proofs10.1145/3497775.3503689(100-115)Online publication date: 17-Jan-2022
https://dl.acm.org/doi/10.1145/3497775.3503689
Parekh SDeshpande APrasanth N(2022)Time Administration of Virtual File System Operations2022 2nd International Conference on Technological Advancements in Computational Sciences (ICTACS)10.1109/ICTACS56270.2022.9987922(555-558)Online publication date: 10-Oct-2022
https://doi.org/10.1109/ICTACS56270.2022.9987922
Tao RYao JLi XLi SNieh JGu R(2021)Formal Verification of a Multiprocessor Hypervisor on Arm Relaxed Memory HardwareProceedings of the ACM SIGOPS 28th Symposium on Operating Systems Principles10.1145/3477132.3483560(866-881)Online publication date: 26-Oct-2021
https://dl.acm.org/doi/10.1145/3477132.3483560
Su WLiu YGanesan GHolzmann GSmolka SZadok EKuenning GShilane PWon Y(2021)Model-Checking Support for File System DevelopmentProceedings of the 13th ACM Workshop on Hot Topics in Storage and File Systems10.1145/3465332.3470878(103-110)Online publication date: 27-Jul-2021
https://dl.acm.org/doi/10.1145/3465332.3470878
Li JMiller SZhuo DChen AHowell JAnderson TAngel SKasikci BKohler E(2021)An incremental path towards a safer OS kernelProceedings of the Workshop on Hot Topics in Operating Systems10.1145/3458336.3465277(183-190)Online publication date: 1-Jun-2021
https://dl.acm.org/doi/10.1145/3458336.3465277
Oberhauser JChehab RBehrens DFu MPaolillo AOberhauser LBhat KWen YChen HKim JVafeiadis VSherwood TBerger EKozyrakis C(2021)VSync: push-button verification and optimization for synchronization primitives on weak memory modelsProceedings of the 26th ACM International Conference on Architectural Support for Programming Languages and Operating Systems10.1145/3445814.3446748(530-545)Online publication date: 19-Apr-2021
https://dl.acm.org/doi/10.1145/3445814.3446748
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents