Jean E. Sammet
Pages 227-228
ACM Ad Hoc Committee on Self-Assessment
Pages 229-235
This paper investigates mechanisms that guarantee secure information flow in a computer system. These mechanisms are examined within a mathematical framework suitable for formulating the requirements of secure information flow …
Dorothy E. Denning
Pages 236-243
A security kernel is a software and hardware mechanism that enforces access controls within a computer system. The correctness of a security kernel on a PDP-11/45 is being proved. This paper describes the technique used to carry …
Jonathan K. Millen
Pages 243-250
The main features of a general purpose multiaccess operating system developed for the CDC 6400 at Berkeley are presented, and its good and bad points are discussed as they appear in retrospect. Distinctive features of the design …
Butler W. Lampson, Howard E. Sturgis
Pages 251-265
This paper describes the design philosophy used in the construction of a family of operating systems. It is shown that the concepts of module and level do not coincide in a hierarchy of functions. Family members can share much …
A. N. Habermann, Lawrence Flon, Lee Cooprider
Pages 266-272
Interesting scheduling and sequential properties of monitors can be proved by using state variables which record the monitors' history and by defining extended proof rules for their wait and signal operations. These two techniques …
John H. Howard
Pages 273-279
An axiomatic method for proving a number of properties of parallel programs is presented. Hoare has given a set of axioms for partial correctness, but they are not strong enough in most cases. This paper defines a more powerful …
Susan Owicki, David Gries
Pages 279-285
The term “locality” has been used to denote that subset of a program's segments which are referenced during a particular phase of its execution. A program's behavior can be characterized in terms of its residence in localities …
A. Wayne Madison, Alan P. Batson
Pages 285-294
An analytical model is presented to estimate the performance of the Page Fault Frequency (PFF) replacement algorithm. In this model, program behavior is represented by the LRU stack distance model and the PFF replacement algorithm …
Wesley W. Chu, Holger Opderbeck
Pages 298-304
Pages 307-308
A criterion for comparing variable space page replacement algorithms is presented. An optimum page replacement algorithm, called VMIN, is described and shown to be optimum with respect to this criterion. The results of simulating …
Barton G. Prieve, R. S. Fabry
Pages 295-297
