NDLI: Freeze after writing: quasi-deterministic parallel programming with LVars

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

Modular reasoning about concurrent higher-order imperative programs

A galois connection calculus for abstract interpretation

Polymorphic functions with set-theoretic types: part 1: syntax, semantics, and evaluation

Tracing compilation by abstract interpretation

A trusted mechanised JavaScript specification

Bias-variance tradeoffs in program analysis

A verified information-flow architecture

Bridging boolean and quantitative synthesis using smoothed proof search

30 years of research and development around Coq

The essence of Reynolds

Freeze after writing: quasi-deterministic parallel programming with LVars

On coinductive equivalences for higher-order probabilistic functional programs

Modular, higher-order cardinality analysis in theory and practice

Optimal dynamic partial order reduction

Authenticated data structures, generically

Parametric completeness for separation theories

From parametricity to conservation laws, via Noether's theorem

Abstract acceleration of general linear loops

Toward general diagnosis of static errors

Battery transition systems

Abstract effects and proof-relevant logical relations

A nonstandard standardization theorem

Backpack: retrofitting Haskell with interfaces

A type-directed abstraction refinement approach to higher-order model checking

An operational and axiomatic semantics for non-determinism and sequence points in C

Abstract satisfaction

CakeML: a verified implementation of ML

A constraint-based approach to solving games on infinite graphs

Replicated data types: specification, verification, optimality

Probabilistic coherence spaces are fully abstract for probabilistic PCF

Profiling for laziness

Modular reasoning about heap paths via effectively propositional formulas

Gradual typing embedded securely in JavaScript

Proof search for propositional abstract separation logics via labelled sequents

A relationally parametric model of dependent type theory

Minimization of symbolic automata

Counter-factual typing for debugging type errors

Symbolic optimization with SMT solvers

Parametric effect monads and semantics of effect systems

Closed type families with overlapping equations

Combining proofs and programs in a dependently typed language

Fissile type analysis: modular checking of almost everywhere invariants

NetKAT: semantic foundations for networks

Proofs that count

Probabilistic relational verification for cryptographic implementations

Sound compilation of reals

Verifying eventual consistency of optimistic replication systems

Tabular: a schema-driven probabilistic programming language

Fair reactive programming

A sound and complete abstraction for reasoning about parallel prefix sums

Sound input filter generation for integer overflow errors

A proof system for separation logic with magic wand

Game semantics for interface middleweight Java

Consistency analysis of decision-making programs

Applying quantitative semantics to higher-order quantum computing

Freeze after writing: quasi-deterministic parallel programming with LVars

Content Provider	ACM Digital Library
Author	Turon, Aaron Krishnaswami, Neelakantan R. Kuper, Lindsey Newton, Ryan R.
Abstract	Deterministic-by-construction parallel programming models offer the advantages of parallel speedup while avoiding the nondeterministic, hard-to-reproduce bugs that plague fully concurrent code. A principled approach to deterministic-by-construction parallel programming with shared state is offered by LVars: shared memory locations whose semantics are defined in terms of an application-specific lattice. Writes to an LVar take the least upper bound of the old and new values with respect to the lattice, while reads from an LVar can observe only that its contents have crossed a specified threshold in the lattice. Although it guarantees determinism, this interface is quite limited. We extend LVars in two ways. First, we add the ability to "freeze" and then read the contents of an LVar directly. Second, we add the ability to attach event handlers to an LVar, triggering a callback when the LVar's value changes. Together, handlers and freezing enable an expressive and useful style of parallel programming. We prove that in a language where communication takes place through these extended LVars, programs are at worst quasi-deterministic: on every run, they either produce the same answer or raise an error. We demonstrate the viability of our approach by implementing a library for Haskell supporting a variety of LVar-based data structures, together with a case study that illustrates the programming model and yields promising parallel speedup.
Starting Page	257
Ending Page	270
Page Count	14
File Format	PDF MP4
ISBN	9781450325448
DOI	10.1145/2535838.2535842
Language	English
Publisher	Association for Computing Machinery (ACM)
Publisher Date	2014-01-11
Publisher Place	New York
Access Restriction	Subscribed
Subject Keyword	Lattices Quasi-determinism Deterministic parallelism
Content Type	Audio 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