Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userDecidability of Liveness on the TSO Memory Model
157
0
0.0
(
0
)
Added by
Yi Lv
Publication date
2021
fields
Informatics Engineering
and research's language is
English
Ask ChatGPT about the research
No Arabic abstract
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.
rate research
Read More
We prove that the genus of a regular language is decidable. For this purpose, we use a graph-theoretical approach. We show that the original question is equivalent to the existence of a special kind of graph epimorphism - a directed emulator morphism -- onto the underlying graph of the minimal deterministic automaton for the regular language. We also prove that the class of directed emulators of genus less than or equal to $g$ is closed under minors. Decidability follows from the Robertson-Seymour theorem.
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.
Codes with various kinds of decipherability, weaker than the usual unique decipherability, have been studied since multiset decipherability was introduced in mid-1980s. We consider decipherability of directed figure codes, where directed figures are defined as labelled polyominoes with designated start and end points, equipped with catenation operation that may use a merging function to resolve possible conflicts. This is one of possible extensions generalizing words and variable-length codes to planar structures. Here, verification whether a given set is a code is no longer decidable in general. We study the decidability status of figure codes depending on catenation type (with or without a merging function), decipherability kind (unique, multiset, set or numeric) and code geometry (several classes determined by relative positions of start and end points of figures). We give decidability or undecidability proofs in all but two cases that remain open.
In the last years, enumeration algorithms with bounded delay have attracted a lot of attention for several data management tasks. Given a query and the data, the task is to preprocess the data and then enumerate all the answers to the query one by one and without repetitions. This enumeration scheme is typically useful when the solutions are treated on the fly or when we want to stop the enumeration once the pertinent solutions have been found. However, with the current schemes, there is no restriction on the order how the solutions are given and this order usually depends on the techniques used and not on the relevance for the user. In this paper we study the enumeration of monadic second order logic (MSO) over words when the solutions are ranked. We present a framework based on MSO cost functions that allows to express MSO formulae on words with a cost associated with each solution. We then demonstrate the generality of our framework which subsumes, for instance, document spanners and regular complex event processing queries and adds ranking to them. The main technical result of the paper is an algorithm for enumerating all the solutions of formulae in increasing order of cost efficiently, namely, with a linear preprocessing phase and logarithmic delay between solutions. The novelty of this algorithm is based on using functional data structures, in particular, by extending functional Brodal queues to suit with the ranked enumeration of MSO on words.
We offer a very simple model of how collective memory may form. Agents keep signalling within neighbourhoods, and depending on how many support each signal, some signals win in that neighbourhood. By agents interacting between different neighbourhoods, influence spreads and sometimes, a collective signal emerges. We propose a logic in which we can reason about such emergence of memory and present preliminary technical results on the logic.
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
