NDLI: Modular verification of concurrent assembly code with dynamic thread creation and termination

Content Provider	ACM Digital Library
Author	Shao, Zhong Feng, Xinyu
Abstract	Proof-carrying code (PCC) is a general framework that can, in principle, verify safety properties of arbitrary machine-language programs. Existing PCC systems and typed assembly languages, however, can only handle sequential programs. This severely limits their applicability since many real-world systems use some form of concurrency in their core software. Recently Yu and Shao proposed a logic-based "type" system for verifying concurrent assembly programs. Their thread model, however, is rather restrictive in that no threads can be created or terminated dynamically and no sharing of code is allowed between threads. In this paper, we present a new formal framework for verifying general multi-threaded assembly code with unbounded dynamic thread creation and termination as well as sharing of code between threads. We adapt and generalize the rely-guarantee methodology to the assembly level and show how to specify the semantics of thread "fork" with argument passing. In particular, we allow threads to have different assumptions and guarantees at different stages of their lifetime so they can coexist with the dynamically changing thread environment. Our work provides a foundation for certifying realistic multi-threaded programs and makes an important advance toward generating proof-carrying concurrent code.
Starting Page	254
Ending Page	267
Page Count	14
File Format	PDF
ISSN	03621340 15581160
DOI	10.1145/1090189.1086399
Journal	ACM SIGPLAN Notices (SIGP)
Volume Number	40
Issue Number	9
Language	English
Publisher	Association for Computing Machinery (ACM)
Publisher Date	1983-05-01
Publisher Place	New York
Access Restriction	One Nation One Subscription (ONOS)
Subject Keyword	Concurrency verification Rely-guarantee Dynamic thread creation Proof-carrying code
Content Type	Text
Resource Type	Article
Subject	Computer Graphics and Computer-Aided Design Software

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

Modular verification of concurrent assembly code with dynamic thread creation and termination

Abstract Modular Verification of Concurrent Assembly Code with Dynamic Thread Creation and Termination

Modular verification of concurrent assembly code with dynamic thread creation and termination.

Verification of safety properties for concurrent assembly code

Modular verification of assembly code with stack-based control abstractions

Modular verification of linearizability with non-fixed linearization points

Proving thread termination

A separation logic for refining concurrent objects

A rely-guarantee-based simulation for verifying concurrent program transformations

Modular verification of concurrent assembly code with dynamic thread creation and termination

Similar Documents

Modular verification of concurrent assembly code with dynamic thread creation and termination

Abstract Modular Verification of Concurrent Assembly Code with Dynamic Thread Creation and Termination

Modular verification of concurrent assembly code with dynamic thread creation and termination.

Verification of safety properties for concurrent assembly code

Modular verification of assembly code with stack-based control abstractions

Modular verification of linearizability with non-fixed linearization points

Proving thread termination

A separation logic for refining concurrent objects

A rely-guarantee-based simulation for verifying concurrent program transformations

Modular verification of concurrent assembly code with dynamic thread creation and termination