# A new thesis concerning synchronised parallel computing - simplified parallel ASM thesis

@article{Ferrarotti2016ANT, title={A new thesis concerning synchronised parallel computing - simplified parallel ASM thesis}, author={Flavio Ferrarotti and Klaus-Dieter Schewe and Loredana Tec and Qing Wang}, journal={Theor. Comput. Sci.}, year={2016}, volume={649}, pages={25-53} }

A behavioural theory consists of machine-independent postulates characterizing a particular class of algorithms or systems, an abstract machine model that provably satisfies these postulates, and a rigorous proof that any algorithm or system stipulated by the postulates is captured by the abstract machine model. The class of interest in this article is that of (synchronous) parallel algorithms. For this class a behavioural theory has already been developed by Blass and Gurevich, which… Expand

#### Topics from this paper

#### 41 Citations

A Behavioural Theory of Recursive Algorithms

- Computer Science
- ArXiv
- 2020

An axiomatic definition of the notion of sequential recursive algorithm is proposed which extends Gurevich's axioms for sequential algorithms by a Recursion Postulate and allows us to prove that sequential recursive algorithms are captured by recursive Abstract State Machines, an extension of nd-seq ASMs by a CALL rule. Expand

A Behavioural Theory of Recursive Algorithms

- Computer Science
- 2020

A language-independent definition of the notion of recursive algorithm generalising Gurevich’s postulates is proposed, and it is proved that recursive algorithms are captured by recursive Abstract State Machines. Expand

A Behavioural Theory for Reflective Sequential Algorithms

- Computer Science
- Ershov Informatics Conference
- 2017

We develop a behavioural theory of reflective sequential algorithms (RSAs), i.e. algorithms that can modify their own behaviour. The theory comprises a set of language-independent postulates… Expand

Behavioural Theory of Reflective Algorithms I: Reflective Sequential Algorithms

- Computer Science
- ArXiv
- 2020

A behavioural theory of reflective sequential algorithms (RSAs), i.e. sequential algorithms that can modify their own behaviour, is developed and the proof that all RSAs are captured by this machine model is proved. Expand

Evolving concurrent systems: behavioural theory and logic

- Computer Science
- ACSW
- 2017

The behavioural theory implies that concurrent reflective Abstract State Machines (crASMs) can be used as a specification and development language for evolving concurrent systems and a logic for crASMs is investigated, based on the simple observation that concurrent ASMs can be mimicked by non-deterministic parallel ASMs. Expand

Computation on Structures - The Challenge of Seamless Integration of Theory and Rigorous Scientific Practice

- Computer Science
- Frontiers in Computer Science
- 2021

The key challenge for theoretical computer science is to provide the necessary scientific foundations centered around computation theory, complexity, and logic, and it has to be ensured that modern computing, in practice with all its facets, is grounded in rigorous scientific methods. Expand

Consistency Enforcement for Static First-Order Invariants in Sequential Abstract State Machines

- Computer Science
- ICFEM
- 2019

The notion of the greatest consistent specialisation (GCS) is adapted and generalised to sequential Abstract State Machines (ASMs) with emphasis on bounded parallelism and it is shown that GCSs are compositional in two respects: the GCS of an ASM with a complex rule can be obtained from the G CSs of the involved assignments. Expand

A unifying logic for non-deterministic, parallel and concurrent abstract state machines

- Computer Science
- Annals of Mathematics and Artificial Intelligence
- 2017

This work develops a logic which enables reasoning about single steps of non-deterministic and parallel Abstract State Machines (ASMs), and shows that the proposed one-step logic can be easily extended to a multiple- step logic which enabling reasoning about concurrent ASMs. Expand

Symbolic execution for a clash-free subset of ASMs

- Computer Science
- Sci. Comput. Program.
- 2018

It is shown that it is possible to compute a first-order formula for each rule that implies clash-freedom when provable, and axioms that describe the transition relation for clash-free ASM rules are given as formulas of predicate logic that can be used to verify pre/post-condition assertions using automated theorem provers. Expand

A Logic for Non-deterministic Parallel Abstract State Machines

- Computer Science
- FoIKS
- 2016

A logic which enables reasoning about single steps of non-deterministic parallel Abstract State Machines ASMs without sacrificing the completeness of the logic for statements about single Steps, such as invariants of rules, consistency conditions for rules, or step-by-step equivalence of rules. Expand

#### References

SHOWING 1-10 OF 34 REFERENCES

Abstract state machines capture parallel algorithms: Correction and extension

- Computer Science
- TOCL
- 2008

The parallel thesis for the new, corrected notion of parallel algorithms is proved, and it is checked that parallel ASMs satisfy the new axioms. Expand

Synchronous Parallel Database Transformations

- Computer Science
- FoIKS
- 2012

The key idea is to generalise the notion of bounded exploration witnesses allowing them to include special non-ground terms in their postulates for synchronous parallel database transformations. Expand

Interactive Small-Step Algorithms I: Axiomatization

- Computer Science, Mathematics
- Log. Methods Comput. Sci.
- 2007

The axiomatization is extended to cover interactive small-step algorithms that are not necessarily ordinary, which means that the algorithms can complete a step without necessarily waiting for replies to all queries from that step. Expand

Parallel Algorithms for Shared-Memory Machines

- Computer Science
- Handbook of Theoretical Computer Science, Volume A: Algorithms and Complexity
- 1990

This chapter discusses parallel algorithms for shared-memory machines, which focus on the technological limits of today's chips, in which gates and wires are packed into a small number of planar layers. Expand

Concurrent abstract state machines

- Computer Science
- Acta Informatica
- 2015

The semantics of concurrent ASMs are defined by concurrent ASM runs which overcome the problems of Gurevich's distributed ASM Runs and generalize Lamport's sequentially consistent runs to form a postulate characterizing an intuitive understanding of concurrency. Expand

A Customised ASM Thesis for Database Transformations

- Computer Science
- Acta Cybern.
- 2010

This paper starts examining the differences between database transformations and algorithms, which give rise to the formalisation of five postulates for database transformations, and proves that every database transformation stipulated by the postulates can be behaviourally simulated by a DB-ASM. Expand

Sequential abstract-state machines capture sequential algorithms

- Computer Science
- TOCL
- 2000

Analysis of the postulates leads to the notion of sequential abstract-state machine and to the theorem in the title. Expand

On Elementary Equivalence for Equality-free Logic

- Mathematics, Computer Science
- Notre Dame J. Formal Log.
- 1996

A model-theoretic study of equality-free logic is worthwhile by itself and it is hoped that the results of this study will contribute to the understanding of the role of equality in mathematical theories and structures. Expand

Abstract State Machines

- Computer Science
- 2003

This chapter describes ASMs as `pseudocode over abstract data’ which comes with a well defined semantics supporting the intuitive understanding, and suggests to skip this chapter and to come back to it only should the need be felt upon further reading. Expand

A Simplified Parallel ASM Thesis

- Computer Science
- ABZ
- 2012

An idea how to simplify Gurevich's parallel ASM thesis is presented, to modify only the bounded exploration postulate from the sequential AsM thesis by allowing also non-ground comprehension terms. Expand