NDLI: Cross-checking semantic correctness: the case of finding file system bugs

Please wait, while we are loading the content...

IronFleet: proving practical distributed systems correct

No compromises: distributed transactions with consistency, availability, and performance

Paxos made transparent

Parallelizing user-defined aggregations using symbolic execution

JouleGuard: energy guarantees for approximate applications

Yesquel: scalable sql storage for web applications

Existential consistency: measuring and understanding consistency at Facebook

Failure sketching: a technique for automated root cause diagnosis of in-production failures

Interruptible tasks: treating memory pressure as interrupts for highly scalable data-parallel programs

How to get more value from your file system directory cache

Using Crash Hoare logic for certifying the FSCQ file system

Implementing linearizability at large scale and low latency

E2: a framework for NFV applications

Read-log-update: a lightweight synchronization mechanism for concurrent programming

Software defined batteries

Building consistent transactions with inconsistent replication

Virtual CPU validation

Cross-checking semantic correctness: the case of finding file system bugs

Chaos: scale-out graph processing from secondary storage

Opportunistic storage maintenance

SibylFS: formal specification and oracle-based testing for POSIX and real-world file systems

Fast in-memory transaction processing using RDMA and HTM

Vuvuzela: scalable private messaging resistant to traffic analysis

Coz: finding code that counts with causal profiling

Drowsy power management

High-performance ACID via modular concurrency control

Holistic configuration management at Facebook

Pivot tracing: dynamic causal monitoring for distributed systems

Arabesque: a system for distributed graph mining

Split-level I/O scheduling

Cross-checking semantic correctness: the case of finding file system bugs

Content Provider	ACM Digital Library
Author	Min, Changwoo Kim, Taesoo Kashyap, Sanidhya Lee, Byoungyoung Song, Chengyu
Abstract	Today, systems software is too complex to be bug-free. To find bugs in systems software, developers often rely on code checkers, like Linux's Sparse. However, the capability of existing tools used in commodity, large-scale systems is limited to finding only shallow bugs that tend to be introduced by simple programmer mistakes, and so do not require a deep understanding of code to find them. Unfortunately, the majority of bugs as well as those that are difficult to find are semantic ones, which violate high-level rules or invariants (e.g., missing a permission check). Thus, it is difficult for code checkers lacking the understanding of a programmer's true intention to reason about semantic correctness. To solve this problem, we present Juxta, a tool that automatically infers high-level semantics directly from source code. The key idea in Juxta is to compare and contrast multiple existing implementations that obey latent yet implicit high-level semantics. For example, the implementation of open() at the file system layer expects to handle an out-of-space error from the disk in all file systems. We applied Juxta to 54 file systems in the stock Linux kernel (680K LoC), found 118 previously unknown semantic bugs (one bug per 5.8K LoC), and provided corresponding patches to 39 different file systems, including mature, popular ones like ext4, btrfs, XFS, and NFS. These semantic bugs are not easy to locate, as all the ones found by Juxta have existed for over 6.2 years on average. Not only do our empirical results look promising, but the design of Juxta is generic enough to be extended easily beyond file systems to any software that has multiple implementations, like Web browsers or protocols at the same layer of a network stack.
Starting Page	361
Ending Page	377
Page Count	17
File Format	PDF MP4
ISBN	9781450338349
DOI	10.1145/2815400.2815422
Language	English
Publisher	Association for Computing Machinery (ACM)
Publisher Date	2015-10-04
Publisher Place	New York
Access Restriction	Subscribed
Content Type	Audio Text
Resource Type	Article

Sl.	Authority	Responsibilities	Communication Details
1	Ministry of Education (GoI), Department of Higher Education	Sanctioning Authority	https://www.education.gov.in/ict-initiatives
2	Indian Institute of Technology Kharagpur	Host Institute of the Project: The host institute of the project is responsible for providing infrastructure support and hosting the project	https://www.iitkgp.ac.in
3	National Digital Library of India Office, Indian Institute of Technology Kharagpur	The administrative and infrastructural headquarters of the project	Dr. B. Sutradhar bsutra@ndl.gov.in
4	Project PI / Joint PI	Principal Investigator and Joint Principal Investigators of the project	Dr. B. Sutradhar bsutra@ndl.gov.in Prof. Saswat Chakrabarti will be added soon
5	Website/Portal (Helpdesk)	Queries regarding NDLI and its services	support@ndl.gov.in
6	Contents and Copyright Issues	Queries related to content curation and copyright issues	content@ndl.gov.in
7	National Digital Library of India Club (NDLI Club)	Queries related to NDLI Club formation, support, user awareness program, seminar/symposium, collaboration, social media, promotion, and outreach	clubsupport@ndl.gov.in
8	Digital Preservation Centre (DPC)	Assistance with digitizing and archiving copyright-free printed books	dpc@ndl.gov.in
9	IDR Setup or Support	Queries related to establishment and support of Institutional Digital Repository (IDR) and IDR workshops	idr@ndl.gov.in

Pallas: Semantic-Aware Checking for Finding Deep Bugs in Fast Path

Maintaining consistency of file system by monitoring file system parameters at runtime using consistency checking rules

Finding complex concurrency bugs in large multi-threaded applications

A Logic of File Systems (2005)

Pallas:Semantic-Aware Checking for Finding Deep Bugs in Fast Path (CARN, Vol. 45, Issue. 1)

Model-checking of correctness conditions for concurrent objects

Finding bugs with a constraint solver

Finding bugs efficiently with a SAT solver

Automatic Checking of the Correctness of Clinical Guidelines in GLARE

Cross-checking semantic correctness: the case of finding file system bugs

Similar Documents

Pallas: Semantic-Aware Checking for Finding Deep Bugs in Fast Path

Maintaining consistency of file system by monitoring file system parameters at runtime using consistency checking rules

Finding complex concurrency bugs in large multi-threaded applications

A Logic of File Systems (2005)

Pallas:Semantic-Aware Checking for Finding Deep Bugs in Fast Path (CARN, Vol. 45, Issue. 1)

Model-checking of correctness conditions for concurrent objects

Finding bugs with a constraint solver

Finding bugs efficiently with a SAT solver

Automatic Checking of the Correctness of Clinical Guidelines in GLARE

Cross-checking semantic correctness: the case of finding file system bugs