NDLI: Subjective auxiliary state for coarse-grained concurrency

Please wait, while we are loading the content...

Engineering mathematics: the odd order theorem proof

Full abstraction for nominal Scott domains

Cache and I/O efficent functional algorithms

Automating relatively complete verification of higher-order functional programs

Quantitative abstraction refinement

The Lambda Lambda-Bar calculus: a dual calculus for unconstrained strategies

The power of parameterization in coinductive proof

From principles to programming languages (and back)

Library abstraction for C/C++ concurrency

The type discipline of behavioral separation

How languages can save distributed computing

Quantitative relaxation of concurrent data structures

Linear dependent types for differential privacy

The principles and practice of probabilistic programming

A model-learner pattern for bayesian reasoning

Sigma*: symbolic learning of input-output specifications

Sub-polyhedral scheduling using (unit-)two-variable-per-inequality polyhedra

The ramifications of sharing in data structures

POPL 2014 Preview

The sequential semantics of producer effect systems

On the linear ranking problem for integer linear-constraint loops

Abstraction and invariance for algebraically indexed types

Inductive data flow graphs

The geometry of types

Meta-theory à la carte

Fault tolerance via idempotence

Views: compositional reasoning for concurrent programs

Plan B: a buffered memory model for Java

Fully abstract compilation to JavaScript

Hyperstream processing systems: nonstandard modeling of continuous-time signals

Checking NFA equivalence with bisimulations up to congruence

Optimizing data structures in high-level programs: new directions for extensible compilers based on staging

Complete instantiation-based interpolation

Copatterns: programming infinite structures by observations

Advanced automata minimization

Static and dynamic semantics of NoSQL languages

Abstract conflict driven learning

Universal properties of impure programming languages

A theorem prover for Boolean BI

Deadlock-freedom-by-design: multiparty asynchronous global programming

High-level separation logic for low-level code

Logical relations for fine-grained concurrency

Towards fully automatic placement of security sanitizers and declassifiers

HALO: haskell to logic through denotational semantics

Synthesis of biological models from mutation experiments

Principled parsing for indentation-sensitive languages: revisiting landin's offside rule

Automatic detection of floating-point exceptions

Subjective auxiliary state for coarse-grained concurrency

Content Provider	ACM Digital Library
Author	Nanevski, Aleksandar Ley-Wild, Ruy
Abstract	From Owicki-Gries' Resource Invariants and Jones' Rely/Guarantee to modern variants based on Separation Logic, axiomatic logics for concurrency require auxiliary state to explicitly relate the effect of all threads to the global invariant on the shared resource. Unfortunately, auxiliary state gives the proof of an individual thread access to the auxiliaries of all other threads. This makes proofs sensitive to the global context, which prevents local reasoning and compositionality. To tame this historical difficulty of auxiliary state, we propose subjective auxiliary state, whereby each thread is verified using a self view (i.e., the thread's effect on the shared resource) and an other view (i.e., the collective effect of all the other threads). Subjectivity generalizes auxiliary state from stacks and heaps to user-chosen partial commutative monoids, which can eliminate the dependence on the global thread structure. We employ subjectivity to formulate Subjective Concurrent Separation Logic as a combination of subjective auxiliary state and Concurrent Separation Logic. The logic yields simple, compositional proofs of coarse-grained concurrent programs that use auxiliary state, and scales to support higher-order recursive procedures that can themselves fork new threads. We prove the soundness of the logic with a novel denotational semantics of action trees and a definition of safety using rely/guarantee transitions over a large subjective footprint. We have mechanized the denotational semantics, logic, metatheory, and a number of examples by a shallow embedding in Coq.
Starting Page	561
Ending Page	574
Page Count	14
File Format	PDF MP4
ISBN	9781450318327
DOI	10.1145/2429069.2429134
Language	English
Publisher	Association for Computing Machinery (ACM)
Publisher Date	2013-01-23
Publisher Place	New York
Access Restriction	Subscribed
Subject Keyword	Dependent type theory Concurrency Local reasoning Rely-guarantee thinking Verification
Content Type	Audio 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

Subjective auxiliary state for coarse-grained concurrency

Local rely-guarantee reasoning

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

Modular fine-grained concurrency verification

Local rely-guarantee reasoning

Rely-Guarantee-Based Simulation for Compositional Verification of Concurrent Program Transformations

Modular verification of linearizability with non-fixed linearization points

A separation logic for refining concurrent objects

Compositional verification of termination-preserving refinement of concurrent programs

Subjective auxiliary state for coarse-grained concurrency

Similar Documents

Subjective auxiliary state for coarse-grained concurrency

Local rely-guarantee reasoning

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

Modular fine-grained concurrency verification

Local rely-guarantee reasoning

Rely-Guarantee-Based Simulation for Compositional Verification of Concurrent Program Transformations

Modular verification of linearizability with non-fixed linearization points

A separation logic for refining concurrent objects

Compositional verification of termination-preserving refinement of concurrent programs

Subjective auxiliary state for coarse-grained concurrency