| 1. |
- Abdulla, Parosh Aziz, Professor, et al.
(författare)
-
Verification of programs under the release-acquire semantics
- 2019
-
Ingår i: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation. - New York, NY, USA : Association for Computing Machinery (ACM). - 9781450367127 ; , s. 1117-1132
-
Konferensbidrag (refereegranskat)abstract
- We address the verification of concurrent programs running under the release-acquire (RA) semantics. We show that the reachability problem is undecidable even in the case where the input program is finite-state. Given this undecidability, we follow the spirit of the work on context-bounded analysis for detecting bugs in programs under the classical SC model, and propose an under-approximate reachability analysis for the case of RA. To this end, we propose a novel notion, called view-switching, and provide a code-to-code translation from an input program under RA to a program under SC. This leads to a reduction, in polynomial time, of the bounded view-switching reachability problem under RA to the bounded context-switching problem under SC. We have implemented a prototype tool VBMC and tested it on a set of benchmarks, demonstrating that many bugs in programs can be found using a small number of view switches.
|
|
| 2. |
- Lööw, Andreas, 1988, et al.
(författare)
-
Verified Compilation on a Verified Processor
- 2019
-
Ingår i: PROCEEDINGS OF THE 40TH ACM SIGPLAN CONFERENCE ON PROGRAMMING LANGUAGE DESIGN AND IMPLEMENTATION (PLDI '19). - New York, NY, USA : ACM. - 9781450367127 ; , s. 1041-1053
-
Konferensbidrag (refereegranskat)abstract
- Developing technology for building verified stacks, i.e., computer systems with comprehensive proofs of correctness, is one way the science of programming languages furthers the computing discipline. While there have been successful projects verifying complex, realistic system components, including compilers (software) and processors (hardware), to date these verification efforts have not been compatible to the point of enabling a single end-to-end correctness theorem about running a verified compiler on a verified processor. In this paper we show how to extend the trustworthy development methodology of the CakeML project, including its verified compiler, with a connection to verified hardware. Our hardware target is Silver, a verified proof-of-concept processor that we introduce here. The result is an approach to producing verified stacks that scales to proving correctness, at the hardware level, of the execution of realistic software including compilers and proof checkers. Alongside our hardware-level theorems, we demonstrate feasibility by hosting and running our verified artefacts on an FPGA board.
|
|
