Modular Verification of Computer Communication Protocols

Programs that implement computer communications protocols can exhibit extremely complicated behavior, and neither informal reasoning nor testing is reliable enough to establish their correctness. In this paper we discuss the application of modular program verification techniques to protocols. This approach is more reliable than informal reasoning, but has an advantage over formal reasoning based on finite-state models, the complexity of the proof need not grow unmanageably as the size of the program increases. Certain tools of concurrent program verification that are especially useful for protocols are presented, history variables that record sequences of input and output values, temporal logic for expressing properties that must hold in a future system state such as eventual receipt of a message), and module specification and composition rules. The use of these techniques is illustrated by verifying two data transfer protocols from the literature: the alternating bit protocol and a protocol proposed by Stenning.     

ALAN: A (Circuit-Switched) Local Area Network

Our view is that people (that is, programmers and general computer users) tend to work together in small groups, where information and resources are shared freely within a group. Most interactions occur within the group (called a cluster)-sending messages, exchanging data, sharing a printer. Communication outside the cluster-sending mail to someone in another group or using a large number cruncher-is comparalively rare. Under this hypothesis, it is advantageous to optimize and simplify interactions within the group. This paper describes our attempt to design a cluster network based on a nonblocking crosspoint switch, which we call ALAN (a local area net). ALAN clusters are star-connected-with intelligent workstation nodes (PC's) at the points of the star, and the ALAN switch at the center.     

Extending objects to support multiple interfaces and access control

A mechanism, called views, that allows programmers to specify multiple interfaces for objects and to control explicitly access to each interface is described. This mechanism provides a simple and flexible means of specifying enforceable access restrictions at many levels of granularity. It also results in system organization that supports browsing based on a number of different criteria. Views is defined, some examples of its uses are given, the impact of views on system organization is discussed, and five approaches to implementing views are outlined     

A Simple Protocol Whose Proof Isn't

Aho, Ullman, and Yannakakis have proposed a set of protocols that ensure reliable transmission of data across an error-prone channel. They have obtained lower bounds on the complexity required of the protocols to assure reliability for different classes of errors. They specify these protocols with finite-state machines. Although the protocol machines have only a small number of states, they are nontrivial to prove correct. In this paper we present proofs of one of these protocols using the finite-state-machine approach and the abstract-program approach. We also show that the abstract-program approach gives special insight into the operation of the protocol.     

Comparing two functional programming systems

A technique is presented for comparing the performance of functional languages with different evaluation strategies running on different machines. A set of small benchmarks is used, and th execution times of these programs running in the functional language and in the implementation language of the functional system are compared. The ratio of these execution times measured how well the functional system used the resources of the underlying hardware and implementation language. Also two functional programming systems are described. One system is a graph reduction interpreter for lambda calculus. The other is a DEL-style intermediate instruction set architecture for FP. The benchmarks in FP and the performances of the two systems on these benchmarks are presented