May 1976 - Vol. 19 No. 5
Features
A lattice model of secure information flow
This paper investigates mechanisms that guarantee secure information flow in a computer system. These mechanisms are examined within a mathematical framework suitable for…
Security Kernel validation in practice
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…
Reflections on an operating system design
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…
Modularization and hierarchy in a family of operating systems
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…
Interesting scheduling and sequential properties of monitors can be proved by using state variables which record the monitors' history and by defining extended proof…
Verifying properties of parallel programs: an axiomatic approach
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…
Characteristics of program localities
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…
MIN—an optimal variable-space page replacement algorithm
A criterion for comparing variable space page replacement algorithms is presented. An optimum page replacement algorithm, called VMIN, is described and shown to be…
Analysis of the PFF replacement algorithm via a semi-Markov model
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…