|Author||Keller, Robert M.|
|Source||ACM Digital Library|
|Publisher||Association for Computing Machinery (ACM)|
|Subject Keyword||Deadlock ♦ Petri nets ♦ Parallel program ♦ Verification ♦ Mutual exclusion ♦ Correctness ♦ Assertions|
|Abstract||Two formal models for parallel computation are presented: an abstract conceptual model and a parallel-program model. The former model does not distinguish between control and data states. The latter model includes the capability for the representation of an infinite set of control states by allowing there to be arbitrarily many instruction pointers (or processes) executing the program. An induction principle is presented which treats the control and data state sets on the same ground. Through the use of “place variables,” it is observed that certain correctness conditions can be expressed without enumeration of the set of all possible control states. Examples are presented in which the induction principle is used to demonstrate proofs of mutual exclusion. It is shown that assertions-oriented proof methods are special cases of the induction principle. A special case of the assertions method, which is called parallel place assertions, is shown to be incomplete. A formalization of “deadlock” is then presented. The concept of a “norm” is introduced, which yields an extension, to the deadlock problem, of Floyd's technique for proving termination. Also discussed is an extension of the program model which allows each process to have its own local variables and permits shared global variables. Correctness of certain forms of implementation is also discussed. An Appendix is included which relates this work to previous work on the satisfiability of certain logical formulas.|
|Description||Affiliation: Princeton Univ., Princeton, NJ (Keller, Robert M.)|
|Age Range||18 to 22 years ♦ above 22 year|
|Education Level||UG and PG|
|Learning Resource Type||Article|
|Publisher Place||New York|
|Journal||Communications of the ACM (CACM)|
Ministry of Human Resource Development (MHRD) under its National Mission on Education through Information and Communication Technology (NMEICT) has initiated the National Digital Library of India (NDLI) project to develop a framework of virtual repository of learning resources with a single-window search facility. Filtered and federated searching is employed to facilitate focused searching so that learners can find out the right resource with least effort and in minimum time. NDLI is designed to hold content of any language and provides interface support for leading vernacular languages, (currently Hindi, Bengali and several other languages are available). It is designed to provide support for all academic levels including researchers and life-long learners, all disciplines, all popular forms of access devices and differently-abled learners. It is being developed to help students to prepare for entrance and competitive examinations, to enable people to learn and prepare from best practices from all over the world and to facilitate researchers to perform inter-linked exploration from multiple sources. It is being developed at Indian Institute of Technology Kharagpur.
NDLI is a conglomeration of freely available or institutionally contributed or donated or publisher managed contents. Almost all these contents are hosted and accessed from respective sources. The responsibility for authenticity, relevance, completeness, accuracy, reliability and suitability of these contents rests with the respective organization and NDLI has no responsibility or liability for these. Every effort is made to keep the NDLI portal up and running smoothly unless there are some unavoidable technical issues.
Ministry of Human Resource Development (MHRD), through its National Mission on Education through Information and Communication Technology (NMEICT), has sponsored and funded the National Digital Library of India (NDLI) project.
For any issue or feedback, please write to email@example.com