NDLI: Expressiveness of Notations for Reasoning about Concurrency

Content Provider	IEEE Xplore Digital Library
Author	Jones, C.B.
Copyright Year	2013
Description	Author affiliation: Sch. of Comput. Sci., Newcastle Univ., Newcastle upon Tyne, UK (Jones, C.B.)
Abstract	It might appear that having highly expressive notations is an advantage in writing specifications and subsequently reasoning about programs. Even for sequential programs, this is not always true: simple type systems that are statically decidable or fixed formats of specifications that yield intuitive proof obligations both indicate that constrained expressiveness can increase tractability. The aim here is to examine some of the trade-offs in expressiveness for notations that address concurrency. The Rely/Guarantee approach to top-down development of concurrent programs offers a way of recording assumptions and commitments about interference. In the same way that pre conditions invite the designer of a component to ignore the possibility that the artifact they are to create will start in states that fail to satisfy the predicate, rely conditions record assumptions the developer is invited to make about any interfering state transitions from the environment in which the artifact will be deployed. In other words, the developer cannot be held liable for the behaviour of the artifact in environments that do not satisfy either assumption. In contrast, just as the post condition expresses a relation that must hold between the initial and final, a guarantee condition records the relation that must exist over any state transition of the artifact. (There are obvious robustness arguments for making components as general as possible; this is not the subject here; it is inevitable that any non-trivial component will need some assumptions.) The decision to use simple relations on pairs of states for (post and) rely and guarantee conditions is a restriction on expressiveness. The restriction, however, means that a reasonably tractable set of proof rules can be given for compositional development of concurrent programs (see [1]; a more recent soundness proof is [2]). In contrast, the initial goal of Concurrent Separation Logic [3] was the bottom-up analysis of intricate code that manipulates heap variables. Here again, there is a deliberate decision to focus on expressing a set of issues: those concerned with separation or ownership. Separation logic has spawned many variants (cf. [4]) but each has a set of operators with neat algebraic properties.
Starting Page	1
Ending Page	1
File Size	87345
Page Count	1
File Format	PDF
e-ISBN	9780769550077
DOI	10.1109/ICECCS.2013.9
Language	English
Publisher	Institute of Electrical and Electronics Engineers, Inc. (IEEE)
Publisher Date	2013-07-17
Publisher Place	Singapore
Access Restriction	Subscribed
Rights Holder	Institute of Electrical and Electronics Engineers, Inc. (IEEE)
Subject Keyword	Concurrent computing Cognition Educational institutions Abstracts Programming Computers abstraction formal methods concurrency
Content Type	Text
Resource Type	Article

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

Reasoning about concurrent objects

Formal Methods for Surviving the Jungle of Heterogeneous Parallelism

Formal Specifications for Java's Synchronisation Classes

Enabling the visualization for reasoning about temporal data

Concurrency in Go and Java: Performance analysis

Proving proof rules: a proof system for concurrent programs

Proving correctness of highly-concurrent linearisable objects

Exploring student understanding of parallelism using concept maps

Task Interaction Graphs For Concurrency Analysis

Expressiveness of Notations for Reasoning about Concurrency

Similar Documents

Reasoning about concurrent objects

Formal Methods for Surviving the Jungle of Heterogeneous Parallelism

Formal Specifications for Java's Synchronisation Classes

Enabling the visualization for reasoning about temporal data

Concurrency in Go and Java: Performance analysis

Proving proof rules: a proof system for concurrent programs

Proving correctness of highly-concurrent linearisable objects

Exploring student understanding of parallelism using concept maps

Task Interaction Graphs For Concurrency Analysis

Expressiveness of Notations for Reasoning about Concurrency