July 1976 - Vol. 19 No. 7
Features
McFarlan and Nolan have made a strong case for adding a course on information systems administration to the 13 courses proposed by the ACM Curriculum Committee on Computer Education for Management for Graduate Professional Programs in Information Systems. This paper is a report on a course entitled, “The Technology of Computer Center Management,” which has been offered at Purdue for the past four years. The course is suitable either for graduate professional programs in information systems or for graduate professional programs in computer science.
Formal verification of parallel programs
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.
Symbolic execution and program testing
This paper describes the symbolic execution of programs. Instead of supplying the normal inputs to a program (e.g. numbers) one supplies symbols representing arbitrary values. The execution proceeds as in a normal execution except that values may be symbolic formulas over the input symbols. The difficult, yet interesting issues arise during the symbolic execution of conditional branch type statements. A particular system called EFFIGY which provides symbolic execution for program testing and debugging is also described. It interpretively executes programs written in a simple PL/I style programming language. It includes many standard debugging features, the ability to manage and to prove things about symbolic expressions, a simple program testing manager, and a program verifier. A brief discussion of the relationship between symbolic execution and program proving is also included.
Ethernet: distributed packet switching for local computer networks
Ethernet is a branching broadcast communication system for carrying digital data packets among locally distributed computing stations. The packet transport mechanism provided by Ethernet has been used to build systems which can be viewed as either local computer networks or loosely coupled multiprocessors. An Ethernet's shared communication facility, its Ether, is a passive broadcast medium with no central control. Coordination of access to the Ether for packet broadcasts is distributed among the contending transmitting stations using controlled statistical arbitration. Switching of packets to their destinations on the Ether is distributed among the receiving stations using packet address recognition. Design principles and implementation are described based on experience with an operating Ethernet of 100 nodes along a kilometer of coaxial cable. A model for estimating performance under heavy loads and a packet protocol for error controlled communication are included for completeness.
Decision tables can be used as an effective tool during an interview to record the logic of processes to be automated. The result of such an interview is not a structure of complete decision tables but rather sets of decision rules. The purpose of this paper is to provide a procedure for synthesizing the decision rules and thus provide an aid in developing a structure of complete decision tables.
Sampling from the gamma distribution on a computer
This paper describes a method of generating gamma variates that appears to be less costly than Wallace's recently suggested method. For large shape parameter &agr;; the cost of computation is proportional to √&agr;, whereas Wallace's method is proportional to &agr;. Experimentation by Robinson and Lewis indicates that for small &agr; the method suggested here also dominates methods recently suggested by Dieter and Ahrens, albeit those methods dominate for large &agr;. The method suggested here uses the rejection technique.
This paper presents a new data structure, called a compressed trie or C-trie, to be used in information retrieval systems. It has the same underlying m-ary tree structure as a trie, where m is a parameter of the trie, but whereas the fields of the nodes in a trie have to be large enough to hold a key or at least a pointer, the fields in a C-trie are only one bit long. In the analysis part of the paper it will be shown that for a collection of n keys the retrieval time, measured in terms of bit inspections of one key, is of the order logmn and the storage requirement of the order n·(m + log2n) bits. This improvement in storage requirements and retrieval time is achieved at the cost of decreasing the flexibility of the structure, and therefore updating costs are increased. First the C-trie is analyzed as a data structure, and then several methods of its use for relatively static databases are discussed.
A buddy system variation for disk storage allocation
A generalization of the buddy system for storage allocation is described. The set of permitted block sizes {SIZEi}ni=0 must satisfy the condition SIZEi = SIZEi-1 + SIZEi-k(i) where k may be any meaningful integral-valued function. This makes it possible to force logical storage blocks to coincide with physical storage blocks, such as tracks and cylinders.
Heaps applied to event driven mechanisms
I read with great interest F.P. Wyman's paper “Improved Event-Scanning Mechanisms for Discrete Event Simulation” [10] which, I found, makes a careful study of some techniques for event-list scanning.
