NDLI: Verification and design aspects of "true concurrency"

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

Compilation and delayed evaluation in APL

The Smalltalk-76 programming system design and implementation

Clauses: scope structures and defined functions in Lucid

Data types as values: polymorphism, type-checking, encapsulation

Type definitions with parameters

Syntactic control of interference

Monoids for rapid data flow analysis

A general scheme for the automatic inference of variable types

Symbolic program analysis in almost linear time

Automatic discovery of linear restraints among variables of a program

A portable compiler: theory and practice

Automating proofs of the absence of common runtime errors

A Metalanguage for interactive proof in LCF

Unrestricted procedure calls in Hoare's logic

A simplifier based on efficient decision algorithms

Reasoning about recursively defined data structures

Off-line and on-line algorithms for deducing equalities

Verification and design aspects of "true concurrency"

Almost control-free (indeterministic) parallel computation on permit schemes

Complexity of expressions allowing concurrency

A partial evaluator, and its use for compiling iterative statements in LISP

Nondeterminism in logics of programs

A straightforward denotational semantics for non-determinate data flow programs

Efficient computation of expressions with common subexpressions

A new method for compiler code generation

A forward move algorithm for LR error recovery

Local constraints in the syntax and semantics of programming languages

Verification and design aspects of "true concurrency"

Content Provider	ACM Digital Library
Author	Mizell, David
Abstract	Most abstract models of a set of parallel processes define a computation of the model to be a sequence. It is either a sequence of actions taken by the system [Lip] or a sequence of states of the system existing between actions [Kel, Lau, Ash]. Parallelsim is represented only by the fact that following a given action or state, the "next" action or state is not necessarily unique. That is, parallesim is represented by nondeterminism. A. W. Holt has called this representation approach "serializable concurrency" as opposed to "true concurrency" [Hol]. He, among others, has questioned the appropriateness of implying a total ordering between events that are only known to be partially ordered.In this paper, a definition of an algebraic model of a set of concurrently-executing sequential processes is presented. The "computations" of this model are directed acyclic graphs. The nodes of each computation graph represent computer operations and the edges represent the partial ordering of operations with respect to time.Examples demonstrate that these directed acyclic graphs aid in focusing a programmer/verifier's attention on the most important features of a computation. The model suggests the following verification paradigm: since systems often execute a certain sequence of actions to achieve a certain goal, verification procedures should identify these sequences, whether or not each is performed within a single process.A key notion in the abstract model is the treatment of synchronization mechanisms as full-fledged processes. A programming language syntax called "path programs" which is suggested by this notion is presented. Path programs are a generalization of the path expressions of Campbell and Habermann [CamHab]. The programming notation is based on the assumption that a processor can be dedicated to each shared data structure in the system. The duty of this processor is to control the synchronization of operations on the data structure.
Starting Page	171
Ending Page	175
Page Count	5
File Format	PDF
DOI	10.1145/512760.512778
Language	English
Publisher	Association for Computing Machinery (ACM)
Publisher Date	1978-01-01
Publisher Place	New York
Access Restriction	Subscribed
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

Views: object-inspired concurrency control

Concurrent aspects

Practical concurrent ASIC and system design and verification

Formal Verification of Real-Time Systems Using a True Concurrency Semantics

Aspects of software design analysis: Concurrency and blocking

Asynchronous games 2 -- the true concurrency of innocence.

Sequential verification of serializability

Teaching concurrency and nondeterminism with spin

Threads as Resource for Concurrency Verification

Verification and design aspects of "true concurrency"

Similar Documents

Views: object-inspired concurrency control

Concurrent aspects

Practical concurrent ASIC and system design and verification

Formal Verification of Real-Time Systems Using a True Concurrency Semantics

Aspects of software design analysis: Concurrency and blocking

Asynchronous games 2 -- the true concurrency of innocence.

Sequential verification of serializability

Teaching concurrency and nondeterminism with spin

Threads as Resource for Concurrency Verification

Verification and design aspects of "true concurrency"