The classical object model supports private data within objects and clean interfaces between objects, and by definition does not permit sharing of data among arbitrary objects. This is a problem for real-world applications, such as advanced financial services and integrated network management, where the same data logically belong to multiple objects and may be distributed over multiple nodes on the network. Rather than give up the advantages of encapsulated objects in modeling real-world entities, we propose a new object model that supports shared data in a distributed environment. The key is separating distribution of computation units from information-hiding concerns. Minimal units of data and control, called facets , may be shared among multiple objects and are grouped into processes . Thus, a single object, or information-hiding unit, may be distributed among multiple processes, or computation units. In other words, different facets of the same object may reside in different address spaces on different machines. We introduce our new object model, describe a motivating example from the financial domain, and then explain facets, objects, and processes, followed by timing and synchronization concerns.

An approach to dynamic reconfiguration in online distributed applications based on a data sharing model is presented. The data sharing model consists of facets, objects, and processes, with facets as the unit of sharing. The primary contribution of this work is the addition of important special cases of dynamic reconfiguration, without resorting to general dynamic allocation. A metaphor consistent with PROFIT's data sharing model for expressing dynamic reconfiguration facilities within the programming language is proposed.>

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 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.>

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.

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.

In this paper, we introduce a new abstraction mechanism, called a script, which hides the low-level details that implement patterns of communication. A script localizes the communication between a set of roles (formal processes), to which actual processes enroll in order to participate in the action of the script. The paper discusses the addition of scripts to the languages CSP and Ada, as well as to a shared-variable language with monitors.

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.

Verifying concurrent systems can be difficult because of the complex interactions possible between system components. In this paper, we propose a technique to simplify the task: modular composition of sequential proofs. We model a parallel program as a set of modules that interact by procedure calls. The properties of each module are proved using a sequential-program verification technique. If the modules satisfy a set of constraints presented in this paper, we may compose the modules into a system and the properties of the modules into properties of the system. The constraints ensure that the specifications are robust for each module where they are defined or used, in the sense that they are unaffected by current actions of other modules. A specification can be guaranteed robust for module m by restricting it to local variables of m, or by using monotonic predicates, which once true remain true forever. Our technique can be used to prove safety and liveness properties of parallel programs---the liveness properties are specified using temporal logic.