RapiLog: Reducing System Complexity Through Verification

Select |




Print


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

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


2013-04-15


Conference Material


EuroSys


Prague, Czech Republic


323-336


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.


operating systems, database systems, ACID properties, durability, virtualization, verification, hypervisor, microkernel


http://eurosys2013.tudos.org/


nicta:6418


Heiser, Gernot; Le Sueur, Etienne; Danis, Adrian; Budzynowski, Aleksander; Salomie, Tudor-Ioan; Alonso, Gustavo. RapiLog: Reducing System Complexity Through Verification. In: EuroSys; Prague, Czech Republic. 2013-04-15. 323-336.



Loading citation data...

Citation counts
(Requires subscription to view)