1996-01-23
1999-02-02
Harrell, Robert B.
G06F 1516
Patent
active
058676490
ABSTRACT:
This invention computes by constructing a lattice of states. Every lattice of states corresponding to correct execution satisfies the temporal logic formula comprising a Definitive Axiomatic Notation for Concurrent Execution (DANCE) program. This invention integrates into a state-lattice computational model: a polymorphic, strong type system; visibility-limiting domains; first-order assertions; and logic for proving a program correctness. This invention includes special hardware means for elimination of cache coherency among other things, necessary to construct state-lattices concurrently. The model of computation for the DANCE language consisting of four, interrelated, logical systems describing state-lattices, types, domains, and assertions. A fifth logical system interrelates the other four systems allowing proofs of program correctness. The method of the present invention teaches programs as temporal formulas satisfied by lattices of states corresponding to correct execution. State-lattices that are short and bushy allow application of many processors simultaneously thus reducing execution time.
REFERENCES:
patent: 4814978 (1989-03-01), Dennis
patent: 4833468 (1989-05-01), Larson et al.
patent: 5029080 (1991-07-01), Otsuki
Reference Manual for the ADA Programming Language, US Dept. of Defense, Jul. 1980.
Communicating Sequential Processes, C.A.R. Hoare, Comm. of the ACM, Aug. 1978, vol. 21, No. 8.
An Optimum Algorithm for Mutual Exclusion in Computer Networks, Glen Ricant et al. Comm. of the ACM, Jan. 1981, vol. 21, No. 1.
An Algorithm for Mutual Exclusion in Decentralized Systems, M. Maekawa, CAM Transactions on Computer Systems, vol. 3, No. 2, May 1985.
The Information Structure of Distributed Mutual Exclusion Algorithms, Sanders, ACM Transactions on Computer Systems, vol. 5, No. 3, Aug. 1987.
A Tree-Based Algorithm for Distributed Mutal Exclusion, K. Raymond, ACM Transactions on Computer Systems, vol. 2, #1, Feb. 1989.
Algorithms for Scalable Synchronization on Shaved Memory Multiprocessors, J. Mollor-Crumley, ACM Transactions on Computer Systems, vol. 9, No. 1, Feb. 1991.
Verification of Sequential and Concurrent Programs, Apt. & Olderog; Springer-Verlag, 1991.
The Science of Programming, D. Gries Springer-Verlag, 1981.
Computer Architecture R. Karin Prentice-Hall (1989) (CPT. 5).
The Design and Analysis of Parallel Algorithms, S. Akl, Prentice-Hall, 1989.
Executing Temporal Logic Programs, B.C. Moszkowski, Cambridge University Press, Copyright 1986, pp. 1-125.
Harrell Robert B.
Multitude Corporation
LandOfFree
Dance/multitude concurrent computation does not yet have a rating. At this time, there are no reviews or comments for this patent.
If you have personal experience with Dance/multitude concurrent computation, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Dance/multitude concurrent computation will most certainly appreciate the feedback.
Profile ID: LFUS-PAI-O-1125368