The global time assumption and semantics for concurrent systems
Shai Ben-David · 1988
We develop a formal model for distributed system executions.Our model helps to bridge the existing gap between formalism and intuition in this field.Our models are built of global rime models (We use the term 'global time model' to denote the intuitive modeling of operation executions as (time) intervals on a straight line).Our semantics is shown to be sound and complete with respect to Lamport's deduction theory 171.Using our semantics we show that arguments that are carried out in global rime models apply to a most general setting.We give a syntactic characterization of a class of issues for which an analysis in global time models suffices.We prove that many questions fall into this class of issues, in particular protocols for implementing atomic registers from safe or regular ones can be analyzed in global time models without losing any generality.(regardless of the number of values or of readers or writers of these registers).