Trustworthy Systems

RapiLog: reducing system complexity through verification

Authors

Gernot Heiser, Etienne Le Sueur, Adrian Danis, Aleksander Budzynowski, Tudor-Ioan Salomie and Gustavo Alonso

NICTA

ETH Zurich

Abstract

Database management systems provide updates with guaranteed durability in the presence of OS crashes or power failures. This is achieved by performing synchronous writes to a transaction log on stable, non-volatile storage. The procedure is expensive and several techniques have been devised to ameliorate the impact on overall performance at the cost of increased system complexity. In this paper we explore the possibility of reducing some of the system complexity around logging by leveraging verification instead of using specialised/dedicated hardware or complicated optimisations. The goal is to study the impact on system design and performance of replacing synchronous writes to the log with a verified system guaranteeing durability. The prototype system developed, RapiLog, uses a dependable hypervisor to buffer log data outside the database system and its OS, and performs the physical disk writes asynchronously to the operation of the database. RapiLog guarantees that the log data will eventually be written to the disk even if the database system or its underlying OS crash. RapiLog can also ensure that in the case of a power failure, all log data is safely written before the system goes down. The implementation uses a hypervisor based on the verified seL4 microkernel and has been tested on three database engines (PostgreSQL, MySQL and a commercial database) on top of Linux. While RapiLog is not yet a complete system and open questions remain, the results show that verified system components can be successfully used to replace intricate system optimisations without compromising overall performance.

BibTeX Entry

  @inproceedings{Heiser_SDBSA_13,
    address          = {Prague, Czech Republic},
    author           = {Heiser, Gernot and Le Sueur, Etienne and Danis, Adrian and Budzynowski, Aleksander and Salomie,
                        Tudor-Ioan and Alonso, Gustavo},
    booktitle        = {EuroSys Conference},
    keywords         = {operating systems, database systems, acid properties, durability, virtualization, verification,
                        hypervisor, microkernel},
    month            = apr,
    pages            = {323--336},
    paperurl         = {https://trustworthy.systems/publications/nicta_full_text/6418.pdf},
    slides           = {https://trustworthy.systems/publications/nicta_slides/6418.pdf},
    title            = {{RapiLog}: Reducing System Complexity Through Verification},
    year             = {2013}
  }

Download