Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userA formalisation of the SPARC TSO memory model for multi-core machine code
120
0
0.0
(
0
)
Added by
Zhe Hou
Publication date
2019
fields
Informatics Engineering
and research's language is
English
Ask ChatGPT about the research
No Arabic abstract
SPARC processors have many applications in mission-critical industries such as aviation and space engineering. Hence, it is important to provide formal frameworks that facilitate the verification of hardware and software that run on or interface with these processors. This paper presents the first mechanised SPARC Total Store Ordering (TSO) memory model which operates on top of an abstract model of the SPARC Instruction Set Architecture (ISA) for multi-core processors. Both models are specified in the theorem prover Isabelle/HOL. We formalise two TSO memory models: one is an adaptation of the axiomatic SPARC TSO model, the other is a novel operational TSO model which is suitable for verifying execution results. We prove that the operational model is sound and complete with respect to the axiomatic model. Finally, we give verification examples with two case studies drawn from the SPARCv9 manual.
rate research
Read More
An important property of concurrent objects is whether they support progress -a special case of liveness-guarantees, which ensure the termination of individual method calls under system fairness assumptions. Liveness properties have been proposed for concurrent objects. Typical liveness properties includelock-freedom,wait-freedom,deadlock-freedom,starvation-freedom and obstruction-freedom. It is known that the five liveness properties above are decidable on the Sequential Consistency (SC) memory model for a bounded number of processes. However, the problem of decidability of liveness for finite state concurrent programs running on relaxed memory models remains open. In this paper we address this problem for the Total Store Order (TSO) memory model,as found in the x86 architecture. We prove that lock-freedom, wait-freedom,deadlock-freedom and starvation-freedom are undecidable on TSO for a bounded number of processes, while obstruction-freedom is decidable.
We present a Coq formalisation of the small-step operational semantics of Jafun, a small Java-like language with classes. This format of semantics makes it possible to naturally specify and prove invariants that should hold at each computation step. In contrast to the Featherweight Java approach the semantics explicitly manipulates frame stack of method calls. Thanks to that one can express properties of computation that depend on execution of particular methods. On the basis of the semantics, we developed a type system that makes it possible to delineate a notion of a compound value and classify certain methods as extensional functions operating on them. In our formalisation we make a mechanised proof that the operational semantics for the untyped version of the semantics agrees with the one for the typed one. We discuss different methods to make such formalisation effort and provide experiments that substantiate it.
Valiant (1975) has developed an algorithm for recognition of context free languages. As of today, it remains the algorithm with the best asymptotic complexity for this purpose. In this paper, we present an algebraic specification, implementation, and proof of correctness of a generalisation of Valiants algorithm. The generalisation can be used for recognition, parsing or generic calculation of the transitive closure of upper triangular matrices. The proof is certified by the Agda proof assistant. The certification is representative of state-of-the-art methods for specification and proofs in proof assistants based on type-theory. As such, this paper can be read as a tutorial for the Agda system.
This work introduces a general multi-level model for self-adaptive systems. A self-adaptive system is seen as composed by two levels: the lower level describing the actual behaviour of the system and the upper level accounting for the dynamically changing environmental constraints on the system. In order to keep our description as general as possible, the lower level is modelled as a state machine and the upper level as a second-order state machine whose states have associated formulas over observable variables of the lower level. Thus, each state of the second-order machine identifies the set of lower-level states satisfying the constraints. Adaptation is triggered when a second-order transition is performed; this means that the current system no longer can satisfy the current high-level constraints and, thus, it has to adapt its behaviour by reaching a state that meets the new constraints. The semantics of the multi-level system is given by a flattened transition system that can be statically checked in order to prove the correctness of the adaptation model. To this aim we formalize two concepts of weak and strong adaptability providing both a relational and a logical characterization. We report that this work gives a formal computational characterization of multi-level self-adaptive systems, evidencing the important role that (theoretical) computer science could play in the emerging science of complex systems.
A common paradigm for scientific computing is distributed message-passing systems, and a common approach to these systems is to implement them across clusters of high-performance workstations. As multi-core architectures become increasingly mainstream, these clusters are very likely to include multi-core machines. However, the theoretical models which are currently used to develop communication algorithms across these systems do not take into account the unique properties of processes running on shared-memory architectures, including shared external network connections and communication via shared memory locations. Because of this, existing algorithms are far from optimal for modern clusters. Additionally, recent attempts to adapt these algorithms to multicore systems have proceeded without the introduction of a more accurate formal model and have generally neglected to capitalize on the full power these systems offer. We propose a new model which simply and effectively captures the strengths of multi-core machines in collective communications patterns and suggest how it could be used to properly optimize these patterns.
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
