In this thesis we investigate the consistency of shared-memory computations from the standpoint of legality. Modeling such systems formally is a fundamental step towards the correct understanding of each model's properties. As the first main contribution of this thesis, we propose a new, two-Ievel (events and operations) formal framework without the undesirable characteristics of architecture dependence, use of global time, or use of totally ordered sets of events or operations. In both levels an execution is represented by a partially ordered set, which gives rise to an AND-OR graph representation from whose structure several properties related to consistency conditions can be deduced. In particular, the existence of b-knots and similar structures is strongly related to the legality of the execution. A second important contribution of this thesis is the introduction of new AND-OR graph structures, such as c-subgraphs, k-components, and the relationship between such structures and knots, b-knots, and cycles.
Our graph-theoretic results are then used to establish a new definition of legality, which, in contrast with the original definition over a sequence of operations, is established over a partially ordered set of operations. We show how this new definition can be used to formally characterize several of the existing consistency models. We conclude that the new formal framework for computations over shared memory and the legality theory introduced in this thesis are suitable to the formal analysis of virtually alI consistency models, as well as to the definition of new ones. They may algo lead to more efficient implementations, since no ordering constraints other than the afies required by each specific model are imposed by the framework itself.