NDLI: Verification of semantic commutativity conditions and inverse operations on linked data structures

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

Commutative set: a language extension for implicit parallel programming

Data representation synthesis

Generalized just-in-time trace compilation using a parallel task farm in a dynamic binary translator

Caisson: a hardware description language for secure information flow

Automatic CPU-GPU communication management and optimization

Understanding POWER multiprocessors

Probabilistic, modular and scalable inference of typestate specifications

Toward generating reducible replay logs

Finding and understanding bugs in C compilers

Spreadsheet table transformations from examples

A security policy oracle: detecting security holes using multiple API implementations

Isolating and understanding concurrency errors using reconstructed execution fragments

Garbage collection for monitoring parametric properties

Cause clue clauses: error localization using maximum satisfiability

Kremlin: rethinking and rebooting gprof for the multicore age

Path-based inductive synthesis for program inversion

Verification of semantic commutativity conditions and inverse operations on linked data structures

Precise and compact modular procedure summaries for heap manipulating programs

Taming the wildcards: combining definition- and use-site variance

Composable asynchronous events

The tao of parallelism in algorithms

Synthesizing geometry constructions

Brainy: effective selection of data structures

Steno: automatic optimization of declarative queries

Automatic compilation of MATLAB programs for synergistic execution on heterogeneous processors

Partial-coherence abstractions for relaxed memory models

Predicate abstraction and CEGAR for higher-order model checking

Higher-order test generation

Evaluating value-graph translation validation for LLVM

Systematic editing: generating program transformations from an example

Language-independent sandboxing of just-in-time compilation and self-modifying code

Automated atomicity-violation fixing

LL(*): the foundation of the ANTLR parser generator

kb-anonymity: a model for anonymized behaviour-preserving test and debugging data

Automatic parallelization via matrix multiplication

Directed incremental symbolic execution

Exploiting the commutativity lattice

On inter-procedural analysis of programs with lists and data

Taming wildcards in Java's type system

Synchronization via scheduling: techniques for efficiently managing shared state

Parallelism orchestration using DoPE: the degree of parallelism executive

Synthesis of loop-free programs

An SSA-based algorithm for optimal speculative code motion under an execution profile

Languages as libraries

EnerJ: approximate data types for safe and general low-power computation

A case for an SC-preserving compiler

Mostly-automated verification of low-level programs in computational separation logic

LeakChaser: helping programmers narrow down causes of memory leaks

Safe optimisations for shared-memory concurrent programs

Cruiser: concurrent heap buffer overflow monitoring using lock-free data structures

NDSeq: runtime checking for nondeterministic sequential specifications of parallel correctness

ALTER: exploiting breakable dependences for parallelization

Mining hot calling contexts in small space

Separation logic + superposition calculus = heap theorem prover

Scaling abstraction refinement via pruning

Verification of semantic commutativity conditions and inverse operations on linked data structures

Content Provider	ACM Digital Library
Author	Kim, Deokhwan Rinard, Martin C.
Abstract	We present a new technique for verifying commutativity conditions, which are logical formulas that characterize when operations commute. Because our technique reasons with the abstract state of verified linked data structure implementations, it can verify commuting operations that produce semantically equivalent (but not necessarily identical) data structure states in different execution orders. We have used this technique to verify sound and complete commutativity conditions for all pairs of operations on a collection of linked data structure implementations, including data structures that export a set interface (ListSet and HashSet) as well as data structures that export a map interface (AssociationList, HashTable, and ArrayList). This effort involved the specification and verification of 765 commutativity conditions. Many speculative parallel systems need to undo the effects of speculatively executed operations. Inverse operations, which undo these effects, are often more efficient than alternate approaches (such as saving and restoring data structure state). We present a new technique for verifying such inverse operations. We have specified and verified, for all of our linked data structure implementations, an inverse operation for every operation that changes the data structure state. Together, the commutativity conditions and inverse operations provide a key resource that language designers, developers of program analysis systems, and implementors of software systems can draw on to build languages, program analyses, and systems with strong correctness guarantees.
Starting Page	528
Ending Page	541
Page Count	14
File Format	PDF
ISBN	9781450306638
DOI	10.1145/1993498.1993561
Language	English
Publisher	Association for Computing Machinery (ACM)
Publisher Date	2011-06-04
Publisher Place	New York
Access Restriction	Subscribed
Subject Keyword	Commutativity condition Verification Data structure Inverse operation
Content Type	Text
Resource Type	Article

Central Library (ISO-9001:2015 Certified)
Indian Institute of Technology Kharagpur
Kharagpur, West Bengal, India | PIN - 721302

See location in the Map
03222 282435
Mail: support@ndl.gov.in

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