1,205 papers · page 54 of 61
In a system based on authorization, the ability of a subject to operate on the system is a function of the privileges that he possesses.In this paper a mechanism, called Send-Receive, for the transport of such privileges, is introduced and studied.The control provided by this mec…
Unlike other instructions, which compute or test values, unconditional branch instructions do no useful work.Rather, they are artifacts of the translation from a flow graph to the linear form of conventional machine language.Careful ordering of the basic blocks of a program can d…
This paper considers a fixed (possibly infinite) set of distributed asynchronous processes, which at various times are willing to communicate with each other.Each process has various ports, each of which is used for communication with a distinct neighbor process.Each process can …
Inference rules are derived for proving partial correctness of concurrent programs that use message passing.These rules extend the notion of a satisfaction proof, first proposed for proving correctness of programs that use synchronous message-passing, to asynchronous message-pass…
A simple definition of the axiomatic semantics of Communicating Sequential Processes is presented.The most important aspect of the approach is that it allows dealing with the individual processes of a program in isolation from the other processes.The axiomatic semantics is used t…
article Free Access Share on Magma2: a language oriented toward experiments in control Author: Franco Turini Univ. di Pisa, Pisa, Italy Univ. di Pisa, Pisa, ItalyView Profile Authors Info & Claims ACM Transactions on Programming Languages and SystemsVolume 6Issue 4Oct. 1984 pp 46…
There are various ways in which programming languages may deal with the use of objects that have no value.They may or may not treat such uses as errors and may or may not trap such errors.The evolution from the preliminary version of Ada TM to the 1980 version and then to the 198…
Writing distributed algorithms in Hoare's CSP becomes more convenient if output statements are allowed in the guards of alternative and iterative commands.The major drawbacks of the previously published implementations of this construct are discussed.Criteria for an effective imp…
CallsThe well-known recursive procedures to compute a given element of the Fibonacci series, to compute a binomial coefficient, and to solve the Towers of Hanoi puzzle define redundant computations.An invocation generally leads to many recursive calls with the same argument value…
The relative efficiencies of four compactors of varisized cells are estimated by constructing their timeformulas.These are symbolic formulas expressing execution times as functions of the time to perform common, elementary operations such as assignment, addition, subscripting, an…
Efficient parallel algorithms to obtain the postfLx and tree forms of an infix arithmetic expression are developed.The shared memory model of parallel computing is used.
The structure of an existing optimizer for the very high-level, set theoretically oriented programming language SETL is described, and its capabilities are illustrated.The use of novel techniques (supported by state-of-the-art interprocedural program analysis methods) enables the…
A distributed algorithm is presented that constructs the minimum-weight spanning tree in a connected undirected graph with distinct edge weights.A processor exists at each node of the graph, knowing initially only the weights of the adjacent edges.The processors obey the same alg…
In this paper the problems of parameter passing and implementation for parameterized algebraic specifications are studied on a proof theoretic level.A syntactic equivalent to the semantic notion of persistency deemed by the ADJ group is introduced for parameterized specifications…
The derivation of machine-specific code optimizers starts from a description of the target machine.A formal instruction-set semantics precisely defmes the concepts characteristic to the machine-code level, such as addressing modes and instructions, side effects, and overlapping o…
In this paper we implement several basic operating system primitives by using a "replace-add" operation, which can supersede the standard "test and set" and which appears to be a universal primitive for efficiently coordinating large numbers of independently acting sequential pro…
The asynchronous execution behavior of several concurrent processes, which may use randomization, is studied.Viewing each process as a discrete Markov chain over the set of common execution states, necessary and sufficient conditions are given for the processes to converge almost…
Pipeline interlocks are used in a pipelined architecture to prevent the execution of a machine instruction before its operands are available.An alternative to this complex piece of hardware is to rearrange the instructions at compile time to avoid pipeline interlocks.This problem…
Development methods for (sequential) programs that run in isolation have been studied elsewhere.Programs that run in parallel can interfere with each other, either via shared storage or by sending messages.Extensions to earlier development methods are proposed for the rigorous de…
A data type specification is a description of the properties of a data abstraction for the benefit of its users and implementers.The data abstraction has realizations, all of which behave in a certain way.It is those properties implied by this behavior which we consider essential…