-
Combining Type Checking and Formal Verification for Lightweight OS Correctness
Authors:
Ramla Ijaz,
Kevin Boos,
Lin Zhong
Abstract:
This paper reports our experience of providing lightweight correctness guarantees to an open-source Rust OS, Theseus. First, we report new developments in intralingual design that leverage Rust's type system to enforce additional invariants at compile time, trusting the Rust compiler. Second, we develop a hybrid approach that combines formal verification, type checking, and informal reasoning, sho…
▽ More
This paper reports our experience of providing lightweight correctness guarantees to an open-source Rust OS, Theseus. First, we report new developments in intralingual design that leverage Rust's type system to enforce additional invariants at compile time, trusting the Rust compiler. Second, we develop a hybrid approach that combines formal verification, type checking, and informal reasoning, showing how the type system can assist in increasing the scope of formally verified invariants. By slightly lessening the strength of correctness guarantees, this hybrid approach substantially reduces the proof effort. We share our experience in applying this approach to the memory subsystem and the 10 Gb Ethernet driver of Theseus, demonstrate its utility, and quantify its reduced proof effort.
△ Less
Submitted 30 December, 2024;
originally announced January 2025.
-
Rio: A System Solution for Sharing I/O between Mobile Systems
Authors:
Ardalan Amiri Sani,
Kevin Boos,
Min Hong Yun,
Lin Zhong
Abstract:
Mobile systems are equipped with a diverse collection of I/O devices, including cameras, microphones, sensors, and modems. There exist many novel use cases for allowing an application on one mobile system to utilize I/O devices from another. This paper presents Rio, an I/O sharing solution that supports unmodified applications and exposes all the functionality of an I/O device for sharing. Rio's d…
▽ More
Mobile systems are equipped with a diverse collection of I/O devices, including cameras, microphones, sensors, and modems. There exist many novel use cases for allowing an application on one mobile system to utilize I/O devices from another. This paper presents Rio, an I/O sharing solution that supports unmodified applications and exposes all the functionality of an I/O device for sharing. Rio's design is common to many classes of I/O devices, thus significantly reducing the engineering effort to support new I/O devices. Our implementation of Rio on Android consists of 6700 total lines of code and supports four I/O classes with fewer than 450 class-specific lines of code. Rio also supports I/O sharing between mobile systems of different form factors, including smartphones and tablets. We show that Rio achieves performance close to that of local I/O for audio, sensors, and modems, but suffers noticeable performance degradation for camera due to network throughput limitations between the two systems, which is likely to be alleviated by emerging wireless standards.
△ Less
Submitted 17 December, 2013;
originally announced December 2013.
-
HEP Applications Evaluation of the EDG Testbed and Middleware
Authors:
I. Augustin,
F. Carminati,
J. Closier,
E. van Herwijnen,
J. J. Blaising,
D. Boutigny,
C. Charlot,
V. Garonne,
A. Tsaregorodtsev,
K. Bos,
J. Templon,
P. Capiluppi,
A. Fanfani,
R. Barbera,
G. Negri,
L. Perini,
S. Resconi,
M. Sitta,
M. Reale,
D. Vicinanza,
S. Bagnasco,
P. Cerello,
A. Sciaba,
O. Smirnova,
D. Colling
, et al. (2 additional authors not shown)
Abstract:
Workpackage 8 of the European Datagrid project was formed in January 2001 with representatives from the four LHC experiments, and with experiment independent people from five of the six main EDG partners. In September 2002 WP8 was strengthened by the addition of effort from BaBar and D0. The original mandate of WP8 was, following the definition of short- and long-term requirements, to port exper…
▽ More
Workpackage 8 of the European Datagrid project was formed in January 2001 with representatives from the four LHC experiments, and with experiment independent people from five of the six main EDG partners. In September 2002 WP8 was strengthened by the addition of effort from BaBar and D0. The original mandate of WP8 was, following the definition of short- and long-term requirements, to port experiment software to the EDG middleware and testbed environment. A major additional activity has been testing the basic functionality and performance of this environment. This paper reviews experiences and evaluations in the areas of job submission, data management, mass storage handling, information systems and monitoring. It also comments on the problems of remote debugging, the portability of code, and scaling problems with increasing numbers of jobs, sites and nodes. Reference is made to the pioneeering work of Atlas and CMS in integrating the use of the EDG Testbed into their data challenges. A forward look is made to essential software developments within EDG and to the necessary cooperation between EDG and LCG for the LCG prototype due in mid 2003.
△ Less
Submitted 5 June, 2003;
originally announced June 2003.
