Philipp Küfner

Uwe Nestmann

Christina Rickmann

Formal Verification of Distributed Algorithms From Pseudo Code to Checked Proofs

We exhibit a methodology to develop mechanically-checkable parameterized proofs of the correctness of fault-tolerant round-based distributed algorithms in an asynchronous message-passing setting. Motivated by a number of case studies, we sketch how to replace often-used informal and incomplete pseudo code by mostly syntax-free formal and complete definitions of a global-state transition system. Special emphasis is put on the required deepening of the level of proof detail to be able to check them within an interactive theorem proving environment.

Introduction

Lamport, Shostak and Pease [LSP82] write about an argument concerning the Byzantine Generals Problem: "This argument may appear convincing, but we strongly advise the reader to be very suspicious of such nonrigorous reasoning. Although this result is indeed correct, we have seen equally plausible "proofs" of invalid results. We know of no area in computer science or mathematics in which informal reasoning is more likely to lead to errors than in the study of this type of algorithm." Along these lines, our goal is to develop mechanically checked proofs about distributed algorithms. In this paper, we address "positive" results on the correctness of problem-solving algorithms, as opposed to "negative" results about the impossibility to solve a problem. We strive for experimental answers to:

-Which description techniques fit best to prove the desired properties of a distributed algorithm when using a theorem prover? -How big is the gap between informal paper proofs and computer-checked proofs? Is the gap merely due to the level of detail that is hidden in words like "straightforward", or is it due to the incompleteness or inadequacy of the model and the used proof techniques?

Fault-Tolerant Distributed Algorithms Any analysis of distributed algorithms is placed within a particular context provided by a system model in which both the algorithm and its specification are to be interpreted. Basic Process Model. We assume a setting of finitely many processes that behave at independent speeds. The controlled global progress of a synchronous system, often paraphrased by means of a sequence of communication rounds, is not available. Moreover, in our model, processes communicate via asynchronous messaging, i.e., without any bound on the delay between emission and reception of messages. Processes typically perform atomic steps consisting of three kinds of actions: (1) input of a message, followed by (2) local computation, followed by (3) output of messages. Starting from some initial configuration of processes and the messaging mechanism, system runs are generated by subsequently performing steps, typically (though not necessarily) in an interleaving fashion. In our model, processes may crash, but do not recover. Here, a process is called correct (in a run) if it does not crash (in this run). In other models, where processes may recover, the notion of processes' correctness needs to be adapted.

Distributed Consensus [Lyn96] (or short: Consensus) is a well-known problem in the field of distributed algorithms: n processes with symmetric behavior, but possibly different initial data, are to commonly decide on one out of several possible values. The task is to find an algorithm satisfying the following three trace properties: (1) Validity: If a process decides a value v, then v was initially proposed by some process. (2) Agreement: No two correct processes decide differently. (3) Termination: Every correct process (eventually) decides some value. Fischer, Lynch and Paterson ([FLP85]) showed that Consensus is not solvable in a fault-prone environment like the above. Essentially, this is due to the fact that in an asynchronous setting, processes that wait for messages to arrive cannot know whether the sender has crashed or whether the message is just late. Often, this is phrased as a lack of synchrony in the communication infrastructure.

Failure Detection and Round-based Solutions. To enhance the setting by some degree of partial synchrony, Chandra and Toueg [CT96] introduced the notion of failure detectors (FD). They allow to determine what is needed to make Consensus solvable in an asynchronous crash-failure environment. A failure detector can be regarded as a local instance at every process that monitors the crash status of all [other] processes. The information provided by the failure detector is usually imperfect, i.e., unreliable to a certain degree. In addition to an enhancement of the model, a common modeling idiom is to use round-based algorithms, which help to simulate the spirit of synchronized executions of the processes to some extent: every process keeps and controls a local round number in its own state. This round number can be attached to messages, which can thereby be uniquely identified. In asynchronous systems, this enables receiving processes to arrange the messages sent by other processes into their intended sequential order. Proofs Revisited. Our set of case studies comprises several distributed algorithms that solve the problem of Consensus for various system models and with varying degree of complexity, taken from [CT96, Lam98,FH07]. For all of these algorithms, proofs of correctness are available, though of quite different level of detail and employing rather different techniques. The proofs often use an induction principle based on round numbers. This counters the fact that executions of distributed algorithms in an asynchronous model do usually not proceed globally round-by-round-which resembles the reasoning in a synchronous model-but rather locally step-by-step. More precisely, the proof does not follow the step-bystep structure of executions, but rather magically proceeds from round to round, while referring to ("the inspection of") individual statements in the pseudo code.

Own Work. Motivated by the lack of formality in typical published proofs of the properties of distributed algorithms, it is part of our own research programme to provide comprehensive formal models and develop formal-but still intuitive-proofs, best mechanically checked by (interactive) theorem provers.

Previous Work. In [FMN07, Fuz08], one of the algorithms of [CT96] and the related Paxos algorithm [Lam98] were presented with a high degree of detail and formality: (i ) the previously implicit setting of the networked processes including the communication infrastructure is made explicit by global state structures; (ii ) the previous pseudo code is replaced by a syntax-free description of actions that transform vectors of state variables; (iii ) the behavior of these two parts is modeled as a labeled global transition system, on which the three trace properties required for Consensus are defined; (iv ) all proof arguments are backed up by explict reference to this transition system.

Contributions.

(1) We demonstrate a method based on the models of [FMN07, Fuz08] to represent distributed algorithms, including the underlying mechanisms for communication and failure detection, together with their respective fairness assumptions, within the theorem-proving environment Isabelle [NPW02]. It turns out that the representation of the transition system specification is quite similar to the syntactic representation of actions in Lamport's Temporal Logic of Actions (TLA) [Lam02], enriched by the notion of global configuration and system runs. (2) We explain how this representation, especially the first-class status of system runs, can be used to verify both safety and -as a novelty-liveness properties within a theorem prover. We argue that, to prove safety properties, it is more intuitive to replace the mere invariant-based style (as exemplified in Isabelle by [JM05]) by arguments that make explicit reference to system runs. Moreover, also to prove liveness properties, explicit system runs represent a convenient proof vehicle. (3) Accompanied by the concrete running example1 inspired by [FH07], we present a formal framework for distributed algorithms and explain techniques for verifying different classes of properties of the algorithm. (4) We give a quick overview of our case studies and provide links to the mechanized proofs in Isabelle. To our knowledge, it is the first time that algorithms from [CT96] have been mechanically checked. In the case of the Paxos proof of [Fuz08], we were able to correct some bugs, while developing the formalization in Isabelle. In contrast, the case study drawn from [FH07] was previously subject to a process-algebraic proof; here, we just used it as a reasonably simple example to demonstrate the quick applicability of our method, small enough to be presented within the space limits of this paper.

Overview of the Paper. In §2, we introduce our formal model based on transition rules and explicit traces that is fundamental for this work. In §3, we present the respective formalization of the required properties. In §4, we discuss how the proof techniques in the respective settings differ, referring to round-based induction and history variables. In §5, we summarize the results of our case studies on doing mechanized proofs for Consensus algorithms. For the sake of readability, we only sketch essential details of the simplest algorithm to demonstrate the method and the shape of the model on which to carry out proofs. Distributed algorithms are often described in terms of state machines [Lam78,Sch90], which are used to capture the individual processes' behavior. As in automata theory, transitions from one state to the next may be given by abstractly named actions. In a more concrete version of this model, states can be considered as vectors of values of the relevant variables and transitions are directed manipulations of these vectors. An essential part of a distributed system is the interprocess communication (IPC) infrastructure, e.g., shared memory, pointto-point messaging, broadcast, or remote procedure calls ([Lyn96]). Thus, the global collection of local state machines for the individual processes must be accompanied by some appropriate representation of the IPC.

Pseudo Code for State Machines

Listing 1.1 exemplifies a common style to present distributed algorithms: a piece of pseudecode that indicates what is executed by each process locally. We use it as a running example to illustrate our experience with Isabelle-checked proofs.

The algorithm solves Consensus in the presence of a strong failure detector (see [CT96] and below). We use process ids (PIDs) p 1 to p n to refer to the n processes. The algorithm proceeds in rounds. For every round, there is one process playing the role of a coordinator. For the given algorithm, coordination means to propose a single value to all processes, while the latter wait for this proposal. The function alive contacts the above-mentioned failure detector to detect the possible failure of the coordinator. The (only) assumption about the failure detector is that at least one correct process is not suspected to be crashed, i.e. the function alive does always return 'True' for some process that never crashes. Correct processes that are not suspected are called trusted-immortal.

Listing 1.1. The Rotating Coordinator Algorithm for participant pi

x i := I n p u t f o r r := 1 to n do { i f r = i then b r o a d c a s t x i ; i f a l i v e ( p r ) then x i := i n p u t f r o m b r o a d c a s t ; } o u t p u t x i ;
As there is no formal semantics and no compiler for pseudo code, formal reasoning is impossible at this level of abstraction. Furthermore, the environment including the IPC-infrastructure (e.g., the various messages in transit) is usually not an explicit part of the pseudo code model. Nevertheless, we choose pseudo code as a starting point for our formalization, as many algorithms are given in this style. Hence, the model is both informal and incomplete; it cannot be transferred into a theorem-proving environment without giving a formal semantics to the usually textual description of actions and not without providing a complete representation of the IPC-infrastructure. We provide a formal model for this example, mention more general modeling aspects and show the key techniques used for the respective correctness proofs.

A i. [[A∈ProcActionSet; A c c i; ProcessState c j = ProcessState c j ]]=⇒ i = j A. [[A∈ComActionSet; A c c ]]=⇒ ProcessState c j = ProcessState c j

State Machines in Isabelle

Fuzzati et al.

[FMN07] define the algorithm in terms of transition rules where the transitions are computation steps between so-called configurations, which represent the global states of the distributed system. In [FMN07], a configuration at time t consists of three components: (1) an array of the local states of the processes, (2) the message history (a set of all point-to-point messages sent until t) and (3) the broadcast history (a set of all broadcast messages sent until t).

The concrete definition of configurations obviously depends on the respective algorithm. To get a general model for distributed algorithms we introduce an abstract type variable configuration. We apply ideas from Merz et al. [CDM11] and model distributed algorithms as interpretations of the locale given in Fig. 1. Locales are used to introduce parameterized modules in Isabelle's theories (see [Bal03]). In the definition of the locale Algorithm, InitPred is a predicate that returns true if a given configuration is a valid initial configuration. ProcAction-Set contains all valid actions that a process can execute: examples are local computations or the sending of messages by placing messages into the local outbox. ComActionSet contains (communication) actions that can be performed independently from a dedicated process (by the system or the communication infrastructure); as an example, imagine the loss of a message during transmission. There is no sense in assigning such an action to the sender or the receiver of the message. Both action sets have to be finite. ProcessState must be instantiated with a mapping that returns a process state for a given configuration and a process. Of course communication actions are not allowed to change the state of any process and performed by some process may not change the state of any other process. This is asserted by StateInv. This allows us to formulate some standard lemmas to be used for each interpretation of the locale. An action A 2). To verify properties of an algorithm, all possible executions of the algorithm must be inspected. We use the term Run for the execution of the algorithm and define it as an infinite sequence of configurations where InitPred holds in the initial configuration and every configuration and its successor is in the step relation. Of course there might be configurations where no further step is possible. In this case the system is deadlocked. For these cases where the actual execution would be finite we allow the system to take stuttering steps, i.e. to repeat the last configuration until the end of time. (see Fig. 2).

R ≡ InitPred (R 0 ) ∧ (∀ t::T . ((R t) → (R (t+1 ))) ∨ FinalStuttering (R t) (R (t+1 )))
IPC The given example requires to implement a message passing mechanism to enable the communication between processes. In our model, a message will traverse three states on its way from the sender to the receiver:

-outgoing: When a sender wants to send a message (or a set of messages) it puts the message into its outgoing buffer. Messages in the outgoing buffer are still at the senders site, i.e. outgoing messages are lost if the sender crashes. -transit: The message is on its way to the receiver.

A crash of the sender does no longer concern messages that are in transit. It is now ready to be processed by the receiver.

We use a multiset-like structure to represent messages in our system, i.e. for every message the number of copies that are outgoing, (respectively transit, received) are stored by mapping messages to records of type MsgStatus, a record that can store a number for each option. For such a mapping we use the term message history. The message history is part of each configuration of our algorithm and represents the state of the message evolution. In our model, sender and receiver are stored for each message. The type Message will later be extended by the payload of the message (depending on the algorithm we want to model). To work with the set of messages (respectively the set of outgoing messages, of transit messages, of received messages) we define functions that return the respective set for a given message history M (see Fig. 3). Now we are ready to define relations between message histories that describe the placement of a message into the outgoing buffer the sending of a message, i.e. the change of status from outgoing to transit the receiving of a message

Our running example requires to put a set of messages in the outbox. Therefore, we define a directive MultiSend : it is a predicate that is true for two message histories M,M and a set of messages msgs if and only if M and M are equal, except for the outgoing values for messages in msgs, which are incremented by one in M . The definitions for changing a message status from outgoing to transit (Transmit) and from transit to received (Receive) are for single messages only and straightforward (see Fig. 4). Note that their preconditions 'm ∈ OutgoingMsgs M' ('m ∈ TransitMsgs M') are necessary to rule out a decrement of zero accidentally generating infinitely many messages.

Rotating Coordinator Model

For the concrete model of our algorithm, we need to define a data structure configuration that contains all relevant information of the system for one point in time. We already identified message histories as one important part of every configuration. Of course, processes can take steps and change their local state without changing the message history (for example, by doing local computations or processing received messages). Hence, another important component of a configuration must be the local states of processes. In our case, the state of a process p i can be defined by five variables: r -The round of p i . phs -The phase of p i , i.e. a next-step indicator. x -The value of the variable x i (cp. listing 1.1) crashed -A flag showing whether p i has crashed. decision -A value that is set from ⊥ to v value when p i decides v.

We use the value P1 in phs if the process is in line 3 and P2 if it is in line 4 (c.p. listing 1.1). We do not need more values, as being in line 6 can be detected by testing if r > n (where n is the number of processes) and the remaining lines are just initialization of variables that will be modeled by the respective InitPred.

As in [FMN07], we use the term program counter for the pair (r, phs). In a configuration, we have to store a process state entry for each process. Hence, we use a mapping from processes to process states as another component of configurations. As explained above, the message type must be extended by the

i v ≡ {m. ∃ j ∈ procs. m = (|snd = i, rcv = j , cnt-v = v |) } definition MsgGen :: configuration ⇒ configuration ⇒ proc ⇒ bool where MsgGen c c i ≡ crashed (St c i) = False ∧ phs (St c i) = P1 ∧ r (St c i) ≤ N ∧ St c = (St c) (i := (| r = r (St c i), phs = P2 , x = x (St c i), crashed = False, decision = decision (St c i) |)) ∧ (if (r (St c i) = PID i) then MultiSend (Me c) (Me c ) (p1msgset i (x (St c i))) else Me c = Me c)
Fig. 6. Definition: Action MsgGen respective payload. In our case, the content a process has to send is its current x value, here of type Input. Hence, the message type is extended by a field cnt-v.

As a result of these considerations, we get the type for a configuration as a record consisting of an array of process states and a message history (see Fig. 5).

Next, we define the communication and process actions. Regarding Listing 1.1 after the initialization, a process p i checks whether it is itself the coordinator of its current round. If so, then it sends a set of messages with p i i as the sender, the current value of x at p i as the content, and all processes as the receivers. p1msgset in Fig. 6 constructs such a set for the respective arguments p i and x.

Based on this definition, for example, the definition of action MsgGen is read as follows: A step from c to c is a MsgGen step taken by p i if and only if

-p i is not crashed in c -phs of p i is P1 in c and P2 in c
r of p i is less or equal than N and is not changed to c x, crashed and decision of p i do not change from c to c states of all other processes do not change a multisend of the respective p1msgset happens from c to c if the current round of the process equals its process id (PID).

We use the Isabelle function update syntax to implement the desired behaviour:

St c = (St c) (i := (| X |) ) denotes the update in (St c) at i to X to yield (St c ).
Thanks to currying in Isabelle, crashed (St c i ) denotes the crashed variable of process p i 's state in configuration c. MsgRcvTrust trusts an awaited sender and receives its message, while MsgRcvSuspect suspects a sender by no longer waiting for its message. Finish implements the decision step of a process and Crash disables a process by setting its crashed variable. There are also the two communication actions MsgSend and MsgDeliver which push messages one step further (from outgoing to transit, respectively from transit to received).

For runs, initial configurations are those where, for all processes p i , (1) (r,phs) is (1,P1 ), (2) x is the input of p i , (3) (crashed,decision) is (false,⊥) and ( 4) for all messages outgoing, transit and received are set to 0.

We define two sets ProcActions and Networkactions and write down the interpretation of the introduced locale Algorithm as RotCoord with St as the required mapping from configuration and processes to process states (given in Fig. 7). Note that proofs for the finiteness of ProcActions and NetworkActions and for the assertions about process states are required. Two lemmas StateInv1 and StateInv2 show that the locale assumption StateInv is satisfied. Validity and Agreement (see the Introduction) are safety properties; as pure invariants of the algorithm they can be formulated as state predicates. Hence, for Validity and Agreement, it would be sufficient to reason about individual states, and whether the properties are preserved by every transition. Termination is a liveness property; it requires us to consider full runs as first-class entities.

We do not include a formulation of Validity in this paper. Instead, next to the formalizations of Agreement and Termination (see Fig. 8), we explicitly mention Irrevocability for decisions, i.e, that decisions cannot be undone or overwritten.

lemma Irrevocability: assumes R: Run R and

d : decision (St (R t) i) = None and z : z ≥t shows the(decision(St (R z ) i)) = the (decision(St (R t) i)) decision (St (R z ) i) = None theorem Agreement: assumes R: Run R and di: decision(St (R t) i) = None and dj : decision(St (R t) j ) = None shows the(decision(St (R t) i)) = the (decision(St (R t) j ))
theorem Termination: assumes R: Run R and i: i

∈ Correct R shows ∃ t. decision (St (R t) i) = None

Proof techniques

'Inspection of the Code' To show that an algorithm exhibits certain properties, we need to refer to its 'code'. Since pseudo code has no formal semantics, this kind of reference cannot be formal. The reader has to believe that certain basic assertions are implied by single lines of the code; e.g., if line 27 states x := 5 then, after line 27 is executed by p i , variable x will indeed have value 5.

Reasoning is done by 'inspection of the code'. For distributed algorithms, this kind of local reasoning is of course error-prone, because one might assume x = 5 when executing line 28, which might be wrong if x is shared and another process changes x while p i moves from line 27 to 28. In [FMN07], the reference to local pseudo code is replaced by the reference to formally-defined global transition rules. Then, if some rule A is provably the only one that changes the variable x of process p i and process p i 's variable has changed from time t x to t then, obviously "by inspection of" the rules, we can infer that A was executed between t x and t. Such a setup is a useful basis for its application within a theorem prover.

Invariant-Based Reasoning This well-known technique boils down to the preservation of properties from one configuration to another during computation steps: essentially, it requires a proof by case analysis for all possible actions in such a step. Here, the formal version of 'inspection of the code' is pertinent. Finding a proof that an invariant property holds in some initial configuration leads to the standard proof technique of induction over time t, i.e., along the configurations of a run, which we evidently use a lot in our examples.

History-Based Reasoning Reasoning along the timeline gets more difficult if also assertions about the past are made. Showing that p i received a message m on its way to configuration c would require to inspect every possible prefix of a run, unless there is some kind of bookkeeping implemented in the model. In [FMN07], this problem is solved by the introduction of history variables [Cli73, Cla78,Cli81] that keep track of events during the execution of the algorithm.

For verification purposes of concurrent programs, history variables are common (see [GL00,Owi76]). Technically, we make history variables an explicit part of our model that also serves for the needed IPC. This provides access to the entire communication history. Every sent message is stored in the history and will not be deleted during a run. Hence, when inspecting a configuration (R t), all messages sent before t are accessible. Therefore, the above-mentioned assertion can be reduced to the simple check that m is in the message history of c.

Application of Proof Techniques

As Validity is an invariant, the technique for invariant-based reasoning is applied. For the used induction principle, it is to show that Validity holds in the initial state of every run and every step of the algorithm preserves it. Hence the main part of the proof is a classical example for the most-used proof technique mentioned above: fix a run R and a time t, then perform induction on t. As a consequence, the remaining proof goals are:

show that for every initial configuration R(0) ∈ Init P (R(0)) holds.

show that P (R(t)) implies P (R(t+1)).

Mostly, the first goal is implied by the definition of the initial states Init. The second goal requires that every defined transition rule preserves P ; the induction hypothesis can be strengthened by the knowledge that the step R(t) → R(t+1) is derived by exactly one application of one of the defined transition rules (distinction of cases). Hence, it remains to show that every application of some rule leads to a successor configuration R(t+1) with P (R(t+1)).

The main argument for Agreement in our running example is that processes cannot skip messages of trusted-immortal processes. Let ti be a trusted-immortal process. We sketch the proof that every process has the same value stored in x before entering a round higher than PID ti (where PID is a function that returns a unique process id from 1..N for every process): Every process j that decides a value must traverse every round number between 1 and n and, therefore, also the round number PID ti where ti is the coordinator. Since j cannot skip the message of a trusted-immortal process, j has to assign the value v ti of ti to its state variable x before entering round (PID ti) + 1. Therefore, afterwards, all processes j in higher rounds than PID ti will send the value v ti or nothing (if they crash before) and, hence, processes can only apply value v ti in such rounds. Formally, this is expressed by the Lemma uniformRndsAfterTI2 asserting that two processes in rounds higher than the process id of some trusted-immortal process must have the same x value. This implies agreement since every process that decides, decides for its x value and must be in round n+1 and n+1 is greater than every process id. Many more invariants must be derived to prove this lemma and both introduced proof techniques are applied in multiple steps.

The proof for Termination appears to be, at first sight, quite obvious: Processes can only block while waiting for messages of trusted-immortal processes. We sketch the proof how mutual waiting is ruled out. Let ti 1 and ti 2 be two trusted-immortal processes waiting for each other's messages. Without loss of generality, let PID ti 1 ≤ PID ti 2 . Since ti 1 waits for the message of ti 2 , it must be in round PID ti 2 and therefore in a round greater than or equal to its own round. Thus, ti 1 already must have sent the message for round PID ti 1 and therefore ti 2 must eventually receive this message.

In our formal model, this proof is quite more difficult. The suggested proof relies on the implicit fairness assumption that every possible process step and every possible message transition from outgoing to transit and from transit to received will eventually happen, which is implicitly implied by the model.

Nevertheless, in the given example, it is possible to give a formal proof without introducing further fairness assumptions about the execution of ProcActions: since we allow FinalStuttering only if no further defined actions are possible, in runs with FinalStuttering, there can be no infinitely enabled actions. Hence, one can prove that every action that is enabled either gets disabled later or is executed later on. The proof of Termination therefore relies on proving two assertions: every run of the algorithm has FinalStuttering and, at the beginning of the FinalStuttering, a correct process is in round number n+1 and therefore has decided (otherwise the action Finish would still be enabled).

More Case Studies

Our much more complicated case studies are two widely known Consensus algorithms: (1) one by Chandra and Toueg [CT96] (thus, from now on referenced as CT) that uses the failure detector 3S-known as the weakest that allows to solve Consensus-and (2) Paxos, by Lamport [Lam98]. The latter does not satisfy Termination, but it does not need failure detectors.

A formal review of both algorithms is found in [Fuz08]. Compared to the running example (Listing 1.1), both cases are much more complex caused by the weaker assumptions on the asynchrony of the environment. For each algorithm, we required approximately 10k LOC in Isabelle/HOL2 . The basic model and the proof techniques are essentially the same except for a few mentionable details.

In the Rotating Coordinator algorithm all n processes decide in the same round (in round n+1), while in Paxos and CT processes might decide in different rounds; also, there is no upper bound for the traversed round numbers. Moreover, processes can decide values broadcast in different rounds. Hence, we need some kind of global view on the system, i.e. to consider whole configurations. For this purpose, already [CT96] introduce the notion of Locked Values. A value is locked for a round r if more than the half of all processes acknowledged the value sent by the coordinator of r. A central lemma for both algorithms states that if v 1 and v 2 are locked values in rounds r 1 and r 2 then v 1 = v 2 . Inspired by the proof sketches in [CT96], Fuzzati et al.

[FMN07] use induction on the round number to prove this lemma: To prove a proposition P holds for all rounds r with r ≥ r the first step is to show P holds for r = r . In the inductive step, P is shown for round k under the assumption that P holds for all r with r ≤ r < k.

Regarding the timeline, this approach dissents from standard temporal reasoning techniques, as the 'global' round number does not proceed consistently with the global clock. In fact, the round number might be different in all local states of the processes and can evolve independently from the global progress as long as it is monotonically increasing; it is possible that a round number r i of process p i is greater than the round number r j of a process j and later in time r i < r j holds. Therefore, proofs done by this technique are intricate, hard to follow by a reader, and not preferred for doing formal proofs. This is documented by errors that we found in [FMN07, Fuz08] (see below). Making such errors within a theorem proving environment is not possible and, hence, we were forced to correct them.

Another difference due to the complexity of Paxos and CT is that there are different types of messages within single rounds; hence, we get dependencies of messages. For example, if message m 2 depends on the prior reception of message m 1 , we can deduce that, if p i sent m 2 to p i , it must have received m 1 . Moreover, the sender of m 1 must indeed have sent m 1 . Thus, new proof patterns arise for dependencies between and also concerning their contents.

One important contribution of the mechanizing proofs is the awareness that even proofs at such a formal level as [Fuz08] can exhibit severe faults without being noticed. During our work, we found several problems both in the model and the proofs. The major problems we found in the proof for Paxos of [Fuz08] are:

-There was an error in the broadcast mechanism that circumvented a delivery of broadcasts to all processes except for its sender and therefore would render executions, where only the minimal majority of processes are alive when the first process decides, nonterminating. Moreover an assumption about the mechanism claimed that every broadcast will eventually be received by all correct processes. Due to the error mentioned before this is in contradiction to the transition rules. Of course from this contradiction one could derive any property needed. -Another problem concerned the basic orderings that are introduced for the reasoning on process states. It turned out that the ordering does not fullfill the required monotoncity in time that was assumed. Since many proofs for the following lemmas relied on this ordering, this problem is serious.

-The proof for one of the central lemmas (Locking Agreement) is wrong.

It uses another lemma (Proposal Creation), but its assumptions are not fullfilled. Therefore, we had to find an adequate version of this lemma with weaker assumptions and redo both proofs (a similar error occurs in [FMN07]).

Conclusion

Exemplified with Consensus algorithms, we show how to represent their widespread informal and incomplete pseudo-code descriptions instead in a formal and complete way that can be processed within a theorem prover. It is not our intention to suggest algorithm designers shall start with pseudo code; we rather show how given pseudo descriptions can be formalized. Furthermore, we may thus point out alternative algorithm representations that can be formalized in theorem proving environments. By intention, our approach (continuing our previous ) is close to the well-known abstract state machines from Gurevich [Gur93], and also actions in the TLA-format, as it is our goal to achieve formalizations of algorithms and their proofs that are reasonably close to the intuitions of typical researchers in the field. The formalization usually requires to add details to the pseudo code so it hardly ever correponds one-to-one. However, this can also be seen as an advantage as it forces to clarify potential sources of misinterpretation. When mechanizing the proofs (or rather: previous proof sketches), we tried to stick to the intuitive arguments and proof techniques as much as possible. Hence automatic tools like Sledgehammer or Quickcheck were not used. But, mechanization requires us to write out all the details; thereby, it proves that the intuitive reasoning (also in our own previous work) is often enough too sloppy.

We report on three case studies within this paper. (1) Our running example is very simple, as it is based on strong assumptions about the system model. We chose it just as a convenient representative for this paper, as it is impossible to show the more interesting case studies within the space constraints. Still, most of the method can be exemplified with it. We found this example in a processalgebraic setting [FH07], and also wanted to be able to roughly compare the amount of work needed in the two completely different settings. We now believe that the approach of the current paper is more intuitive-and mechanized!-and thus leads to quicker proofs. (2) The CT-algorithm has now, to our knowledge the first mechanically-checked proofs, including Termination. The latter is only possible, as our formal model includes an explicit representation of runs. (3) The Paxos algorithm can, modulo some changes to the model, be seen as a variant of CT. As mentioned before, the work on Disk Paxos in [JM05] is quite similar to our work for safety properties. The main difference is based on the different model that allows us to comfortably prove liveness properties in the case of CT.

Fig. 1 .

 1 Fig. 1. Locale for Distributed Algorithm

definition

  LocalStep:: configuration ⇒ configuration ⇒ bool where LocalStep c c ≡ ∃ i ∈ procs. ∃ A ∈ ProcActionSet. A c c i definition ComStep:: configuration ⇒ configuration ⇒ bool where ComStep c c ≡ ∃ A ∈ ComActionSet. A c c definition Step:: configuration ⇒ configuration ⇒ bool (infixl → 900 ) where Step c c ≡ LocalStep c c ∨ ComStep c c definition deadlock :: configuration ⇒ bool where deadlock c ≡ ∀ c . ¬ c → c definition FinalStuttering :: configuration ⇒ configuration ⇒ bool where FinalStuttering s s ≡ (s = s ) ∧ deadlock s definition Run :: (T ⇒ configuration) ⇒ bool where Run

Fig. 2 .

 2 Fig. 2. Definition: Steps and Runs

  Fig. 3. Messages

definition

  Fig. 4. Message movements

  Fig. 5. Definition: configuration definition p1msgset :: proc ⇒ Input ⇒ msg set where p1msgset i v ≡ {m. ∃ j ∈ procs. m = (|snd = i, rcv = j , cnt-v = v |) }

  Fig. 7. Interpretation RotCoord

Fig. 8 .

 8 Fig. 8. Irrevocability, Agreement and Termination

full details at http://www.mtv.tu-berlin.de/fileadmin/a3435/Isa/RotCoord.zip

full models and proofs can be found at http://www.mtv.tu-berlin.de/fileadmin/a3435/Isa/CT.zip http://www.mtv.tu-berlin.de/fileadmin/a3435/Isa/Paxos.zip


Jiří Wiedermann
email: jiri.wiedermann@cs.cas.cz

Computability and Non-Computability Issues in Amorphous Computing

Amorphous computing systems consist of a huge set of tiny simple stationary or mobile processors whose computational, communication and sensory part is reduced to an absolute minimum. In an airborne medium the processors communicate via a short-range radio while in a waterborne medium via molecular communication. In some cases the computational part of the processors can be simplified down to finite state automata or even combinatorial circuits and the system as a whole can still possess universal computational power with a high probability. We will argue that the amorphous systems belong among the simplest (non-uniform) universal computational devices. On the other hand, it is questionable as to what extent the standard universal models of computation can faithfully capture the behavior of amorphous computing systems whose functionality also depends on the non-computational and/or unpredictable operations of certain parts of the entire system.

Introduction

The notion of amorphous computing systems, i.e., of computational systems lacking any concrete "architecture", has emerged by the end of the 1990's. Initially, the development of such systems started as an engineering enterprise motivated by technological advancement in the field of micro-electro-mechanical systems, wireless communications and digital electronics (cf. [START_REF] Abelson | Amorphous Computing[END_REF], [START_REF] Abelson | Amorphous Computing[END_REF], [START_REF] Arvind | Speckled Computing A Disruptive Technology for Network Information Appliances[END_REF], [START_REF] Coore | Introduction to Amorphous Computing[END_REF], [START_REF] Kahn | Next century challenges: mobile networking for "Smart Dust[END_REF], [START_REF] Kahn | Emerging Challenges: Mobile Networking for Smart Dust[END_REF], [START_REF] Sailor | Smart dust: nanostructured devices in a grain of sand[END_REF], [START_REF] Shah | Speckled Computing: Evolution and Challenges[END_REF], [START_REF] Warneke | Smart Dust: communicating with a cubicmillimeter computer[END_REF]). Technological progress enabled integration of sensing, data processing and wireless communication capabilities into a single processor. In these systems the miniaturization has been pushed to its limits resulting, presumably, into processors of almost molecular size with the respective communication and computing facilities adequately (and thus, severely) restricted. These limitations alone, and the fact that systems consisting of huge numbers of processors are considered, have jointly called for the change of the basic computational and communication paradigms of distributed computing systems. These new paradigms also seem to have a potential to challenge certain computability issues related to our understanding of computing.

Nowadays we see amorphous computing systems in many forms (cf. [START_REF] Wiedermann | The Many Forms of Amorphous Computational Systems[END_REF]). Amorphous computing systems typically consist of a huge set of tiny simple processors This work was partially supported by RVO 67985807 and the GA ČR grant No. P202/10/1333 equipped with small memory, random number generator, simple wireless communication means, sensors and an energy source. The processors are randomly distributed over a closed area in which they can move, or are static. In the former case, the processors move by their own locomotion means, or by external forces, like Brownian motion, wind or stream. In an airborne medium the processors communicate via radio while in a waterborne medium via molecular communication. Moreover, in order to operate as envisaged some amorphous computing systems may exploit non-computable features, i.e., operations that cannot be realized computationally, such as self-replication or disintegration.

In this note we will focus our attention on specific instances of amorphous computing systems by which we will illustrate some remarkable aspects of amorphous computing systems.

First, we will be interested in their universality, i.e., in their ability to simulate arbitrary computations (of a Turing machine, say). Namely, for some amorphous computing systems this ability is by far not obvious due to the drastic restrictions imposed on computational and communication parts of the system's processors.

Strictly speaking, many (envisaged) applications of amorphous systems do not require universality. Single-purpose systems enabling, e.g., centralized data collection, a geographic area monitoring, intra-body multi-modal health monitoring, or drug delivery to certain body locations, often do. Nevertheless, universality qualifies these systems among the programmable systems which are, in principle, capable to perform an arbitrary algorithmic or even robotic task.

The second intriguing feature which we will be interested in is the problem of the reverse simulation of amorphous computing systems by standard models of universal computations. Namely, by their very nature, some amorphous computing systems are in fact described as physical (rather than purely computational) systems whose operation also depends on abilities of their processors and those of their environment that are of non-computational nature. This appears to be a serious obstacle for their faithful simulation on standard computational devices.

In the sequel, in Section 2 we will briefly describe two relatively advanced and unusual amorphous computing systems: an airborne, so-called flying amorphous computing system, and a waterborne system, so-called nanomachines. Here we will only provide a high-level description of the respective machines and of their computational and non-computational mechanisms in order to give the reader the main ideas of their functioning. In a more detail these systems have been introduced in earlier writings of the present author (cf. [START_REF] Petrů | A Universal Flying Amorphous Computer[END_REF], [START_REF] Wiedermann | Nanomachine Computing by Quorum Sensing[END_REF]). Based on the previous descriptions, we will discuss the related universality issues in Section 3. In Section 4 we will concentrate on the problem of a reverse simulation of the previously described amorphous systems on a universal computational model. Conclusions are in Section 5.

2 Universality in Amorphous Computing Systems

Flying Amorphous Computer

A flying amorphous computer consists of a set of asynchronous processors. Each processor posses a clock running with the same speed as all the other processors; however, the "ticking" of all clocks is not synchronized. Each processor is modeled by a "miniature" RAM with a finite number of registers capable of storing integers up to size N, with N denoting the number of nodes of the underlying amorphous system. Each processor is equipped by a random number generator and a single-channel radio device of a limited communication range. Initially, the processors have no unique identifier.

A severe restriction is imposed on the communication abilities of processors. A processor P 1 could receive a message sent by processor P 2 if and only if the following conditions hold true: (i) the processors are in the communication range of each other, (ii) P 1 is in a listening mode, and (iii) P 2 is in a broadcast mode, and it is the only processor within the communication radius of P 1 broadcasting at that time.

There is no mechanism making it possible to distinguish the case of no broadcast from that of broadcast collision. These restrictions concerning the radio communication are among the weakest ones that one can expect to be fulfilled by any simple radio communication device. The expected benefit from such restrictions is a simple engineering design of processors.

Note that the communication among the processors is complicated by the fact that the processors work asynchronously, have no identifiers, communication is one-way only, and there is no broadcast collision detection mechanism. As long as the processors remain anonymous (i.e., have no identifiers) a broadcasting processor has no means to learn that its message has been received by some processor. Under such circumstance, the randomized protocol designed in [START_REF] Petrů | A Model of an Amorphous Computer and Its Communication Protocol[END_REF] enabling a reliable delivery of a message among processors within the communication range of each other works with a high probability, as follows.

The key idea is that the processors should broadcast a message sporadically in order to prevent message delivery (i.e., broadcast) conflicts, and repeatedly in order to maximize the likelihood of a successful delivery. The analysis of such a protocol reveals that the probability of sending should depend inversely on the expected number of a node's neighbors and should be repeated more times to handle the case of more processors in a node's neighborhood (cf. [START_REF] Wiedermann | On the Universal Computing Power of Amorphous Computing Systems[END_REF]). Now, let us assume that cN of such processors, c > 1, fly around randomly in a confined convex volume. They form a dynamic network with a variable topology. The nodes of the network are created by processors with wireless communication links emerging asynchronously among the processors that find themselves within the communication radius of each other and fulfill the restriction for a successful one-way communication mentioned before. Our goal is to program the processors in such a way that they all together can simulate a RAM with N registers. Doing so, each RAM register will be represented in one processor of the flying computer.

The main problem is to keep the system operating under steadily changing topology of the communication network where new communication paths emerge, while the previous ones vanish. Some nodes may even become temporarily inaccessible since they may not find themselves within the communication range of other nodes. The latter problem can be solved under the assumption that no node in the network remains for ever isolated.

Thanks to this assumption, once processors do possess unique addresses, a message sent to a node with a given address would in a finite time reach this node and this node could send an acknowledgment that in a finite time will reach the sender.

The schema of the simulation is as follows. There is one specific node, a so-called leader. First, the leader invites all nodes to generate a random number within the range [1..cN ]. Such an invitation is realized by "flooding" the net by an appropriate signal reaching all nodes with a high probability using the previously described protocol. Doing so, we cannot make use of the acknowledgments (since addresses are not yet available) and therefore a sufficient time must be allowed for the signal to spread over the entire volume with a high probability. Once the addresses are generated, the acknowledgment mechanism is used in all subsequent computations. Next, the duplicates are eliminated by a randomized algorithm described in [START_REF] Petrů | A Universal Flying Amorphous Computer[END_REF] and the addresses are transformed into the range [1..N ]. Now the simulation itself can start. It is a relatively straightforward procedure in which the next step is initiated by the leader only after the sender (i.e., the leader) obtains an acknowledgment from the receiver.

Although the whole system can correctly simulate a RAM (with a bounded memory size) with arbitrary high probability, the simulation time cannot be bounded by any function. However, if the address assignment process is successful (and this can be guaranteed with an arbitrary large probability), the simulation terminates within a finite time and always delivers the correct result. This computer has been described in full detail in [START_REF] Petrů | Universality in Amorphous Computing[END_REF] and later it was presented in [START_REF] Petrů | A Universal Flying Amorphous Computer[END_REF].

Nanomachines

Recent unmatched improvements in nanotechnologies have enabled serious consideration of nano-scale machines whose size is of order 10 -6 mm. Their prospective fabrication will make use of molecular self-assembly or of modifications of real bacteria via genetical engineering. To get an idea about the dimensions of objects we are considering, the size of a real bacteria is of the order of a few micrometers (i.e., of thousandths of millimeter, 10 -6 m) while the size of a molecule is of the order of nanometers (i.e., 10 -9 m). Thus, a nanomachine is about 1000 times bigger than a molecule and its surface and volume is still larger by a few orders of magnitude.

Next we will briefly describe so-called self-reproducing mobile embodied automata (nanomachines for short) whose information exchange mechanism is based on molecular communication.

Each nanomachine consists of two main components: there is its embodiment -the body, and its computational part.

The embodiment of any nanomachine consists of a set of receptors and emitters (pores), internal sensors, a set of timers, a self-reproducing mechanism, random bit generator and possibly of other devices depending on the type of embodiment (e.g., locomotive organs in the form of flagella, cilia, etc.).

Each receptor is specialized for detection of a specific type of molecules. These molecules find themselves in the environment surrounding the machine. Both the machines and the molecules move by convection (diffusion and advection). Moreover, the nanomachines can also move by their own means. For each type of molecules each nanomachine has at its disposal several tens of receptors; their exact number is irrelevant. A molecule gets recognized only in the case when it enters into contact with the respective receptor. Timers are internal mechanisms ("organs") without any external input. Each timer is preset for a fixed time. Each timer returns either 0 or 1. A timer can be reset to 0 by the machine's finite state control. Upon expiration of time for which the timer has been initially set the timer returns 1. Values to which the timers are preset depend on the type of a timer as well as on the properties of the environment (especially on its volume, but also on the properties of some molecules detected by the sensors -e.g., on the degradation time of the molecules). Timers of the same type are the same in all nanomachines.

The self-reproducing mechanism is a non-computational mechanism which is triggered by automaton entering a special reproducing state. In such a case, the nanomachine splits into two identical copies of itself, with their finite controls entering the initial state.

The random bit generator is an "organ" that upon each activation returns either 0 or 1 with the same probability.

The computational part of each nanomachine is created by a finite-state (Mealy) automaton whose actions are controlled by a transition function. In a single move each automaton reads its inputs obtained from its receptors and from other sensors or organs. Depending on these inputs and on its current state, the automaton issues instructions for the machine's organs concerning their next actions: releasing the molecules from the receptors, secreting signal molecules via the pores (output ports), resetting the timers, and instructing its locomotive organs. Last but not least, the control enters a new (possibly a reproduction) state. The use of timers and of a random number generator effectively turns the automata at hand into timed probabilistic automata.

Thus, the instructions for the machines are transmitted via elements from a finite set of molecular signals. Prior to sending a new signal, the environment must be cleared of the previous signal molecules. This is done by endowing the molecules with a certain self-destruction ability -after a certain time they spontaneously disintegrate into components that are not interpreted as any signals. These components are continuously absorbed by nanomachines and re-cycled inside their bodies in order to produce other molecular structures.

During their operation the self-reproducing mobile nanomachines communicate via so-called quorum sensing, i.e., by making collective decisions based on the density of nanomachine population. This density is inferred from the concentration of signal molecules emitted by the machines within a confined space.

In a given volume the machines multiply and emit the signal molecules until their maximal concentration has been reached. Then, they make a collective decision in which they simulate one step of a counter automaton. The resulting amorphous system was shown to be able to model a counter automaton [START_REF] Wiedermann | Nanomachine Computing by Quorum Sensing[END_REF], [START_REF] Wiedermann | Computability in Amorphous Structures[END_REF]. Thus, sequences of nanomachine populations of growing size obey a universal computing power.

Except of the timers and an organ serving as a random bit generator a further modification of the embodiment of the underlying automata may include a memory organ. Then, the task of memorizing the current state can be delegated to that organ. Conse-quently, the computational mechanism of each nanomachine could be simplified down to combinatorial circuits of bounded depths (circuits from the complexity class AC 0 ).

The last mentioned model is of interest not only from a practical point of view, since it could lead to a simpler engineering of nanomachines, but also from the viewpoint of the theory of universal computing machines, as we will see in the sequel.

3 What is the simplest universal computational model? For many computer scientists, a Turing machine, or a counter machine (also known as Minsky machine [START_REF] Minsky | Computation: Finite and Infinite Machines[END_REF]) is considered as the simplest computational model possessing a universal computing power. In fact, there exists a plethora of universal computational devices and it is a matter of taste to select the simplest one from among those models. As a rule, they are represented by the devices with a fixed rigid architecture that enables them to enter configurations from a potentially infinite set of configurations: they are, in fact, infinite automata. None finite device (finite even in the physical meaning of this word) can subsequently enter an unbounded number of different configurations. Inevitably, the size of the device must grow with the number of reachable configurations. This is also the case of the cellular automata possessing a universal computing power. Note that for each input the corresponding cellular automaton is finite; however, the number of its elements grows with the input size.

The next (in)appreciable property of the known universal computational systems is their "non-homogeneity" -they cannot be disassembled into smaller, in some sense elementary identical computational parts that could be reassembled in an arbitrary manner so as to give rise to a universal computing system. A partial departure from this rule is given by cellular automata that almost satisfy our requirement of homogeneity. Clearly, a cellular automaton can be disassembled into individual finite automata. It is obvious that finite automata are simpler computational devices than, e.g., Turing machinesthey only accept regular languages and, therefore, are not universal. Nevertheless, upon a re-assemblage into a cellular automaton one must respect the original topology of the underlying network although the individual automata need not be returned to their original positions -they can be interchanged at wish. Then a universal computing power "emerges" again. Note that in the latter case the universal computing power will not emerge from among any (multi)set of arbitrarily connected finite automata -the condition for that to happen is that the the communication links among the automata must follow a certain regular pattern.

The last consideration brings us to the following reformulation of the question from the title of this section: does there exist a simple computational device whose multisets possess universal computational power even when there is no fixed topology of communication links among their individual elements?

The answer to this question had been prepared in the previous two subsections. Both flying amorphous computers and the nanomachines are the candidates for such devices. This answer must further be stated more precisely. First, in order to ensure that computations of arbitrary space complexity could be realized we must always speak of sequences (or populations) of growing size of such systems. (The corresponding devices are called non-uniform computational devices.) Second, we can only speak of simulations achieving their goal with a high probability.

If we had to make a choice between the two amorphous computing systems standing as candidates for the position of the simplest universal computing device the priority should probably be given to the population of nanomachines controlled by circuits. This is because their activity is governed by the simplest computing devices (viz. circuits). However, there is a price we have to pay for this simplicity. This is the fact that in addition to the purely computational part there is a non-computational mechanism comprising the "body" of the corresponding units of the system. In both cases, this body mainly consists of a communication mechanism, and in the case of nanomachines, the body also contains other, more complicated non-computational components, such as a self-reproducing mechanism, locomotive organs, etc. Moreover, in the case of nanomachines, a "collaboration" of the signal molecules -their disintegration in due time, was necessary. The operation of the system as a whole has been achieved by cooperation and orchestration of activities of all participating components controlled by computational parts of the units. From this point of view, cellular automata can bee seen as highly idealized models of amorphous systems considered in this paper in which it has been abstracted from the embodiment and communication mechanisms.

We conclude that amorphous computing systems considered above belong among the simplest (non-uniform) universal computing devices since their functionality is fully defined by the functionality of any of its parts, and there is no need to describe the "architecture" of the system as a whole.

The Problematic Simulation of Amorphous Systems by Turing Machines

When speaking about the universal computing power of amorphous computing systems in the previous sections we indicated how such systems can simulate devices which are already known to possess such a power. For the purpose of their reverse simulation, thanks to their embodiment and many non-computational features, amorphous computing systems should better be regarded as physical, rather than abstract mathematical systems. Thus, in this case, simulation should bridge the gap between a physical system and an abstract mathematical system. The crux of the problem is that behavior of the underlying physical system cannot be formally described down to the smallest detail. This is a source of difficulties when considering the reverse simulation of amorphous computing systems on universal models of computation. What we have to do in this case is to duplicate, or imitate the functioning of amorphous computing systems on some formal model of computation in such a way that the behavior of the latter system closely mimics the observed behavior of the former system. Unfortunately, this appears to be practically impossible due to the unpredictable behavior of important elements of amorphous computing systems. For instance, in the case of flying amorphous computer, the trajectories of processors are continuous and random as well as the asynchronous communication activities of processors. All these activities run in parallel and concurrently. Moreover, e.g., in the case of nanomachines, the degree of parallelism increases with time (in the first phase of rising up the popula-tion of nanomachines). There are additional parallel processes running at each nanomachine (such as signal molecules sensing/emitting) and also those corresponding to the interactions of molecules in the environment. The disintegration processes of signal molecules must also be taken into account. It is difficult to imagine how emulation of such processes could run on a sequential computer (or any other computer with a bounded parallelism) keeping track of a potentially unbounded number of spatially and temporally related physical variables. Discretization of continuous processes underlying the operation of amorphous computing systems (e.g., think of the movement of the processors) within a discrete computational model, asynchronicity and a potentially unbounded parallelism may thus introduce unsurmountable timing problems for simulation of such processes.

These facts challenge the popular belief that any physical computational device can be emulated within any other, and especially, within any universal model of computation (cf. [START_REF] Nagy | Time inderterminacy, non-universality in computation, and the demise of the Church-Turing thesis[END_REF] and the references therein).

Amorphous computing systems also offer an interesting answer to the question "what everything can compute?". At the same time, they seem to present an example of computations that is captured neither by Turing machines nor by any of their parallelized or other known variants. Obviously, any answer to the question "what is computation?" should also cover computations of amorphous computing systems.

Conclusions

Amorphous computing systems confront us with an interesting dichotomy. They harness non-computational mechanisms for the purpose of computing, but they also exploit computing in order to control these non-computational mechanisms. Thus, amorphous computing systems present a class of computing systems in which physical aspects, manifested through their embodiment, play an important role. Amorphous computing systems can be proved to be computationally universal with a high probability. The respective proofs can come through thanks to focusing to certain computational aspects of their functionality and postulating the expected outcomes of non-computational operations that also contribute to the mechanism of computation. Thus, when reasoning about computational universality of amorphous systems we reason, in fact, about a more abstract, simplified, often probabilistic model of an amorphous system.

The situation changes when we want to capture the behavior of a "real" amorphous computing system (as opposed to that of its model) on a universal computer. This might be the case when we want, e.g., to tune some physical parameters of an amorphous system in order to achieve its better practical performance. In such a case, we have to simulate the physical system as it is, i.e., inclusively of its non-computational aspects which are important for keeping the entire system performing its computational task. The non-computational aspects are determined by complex physical and in some cases, also chemical interactions among the basic elements of amorphous systems which cannot be described as computational processes.

An additional problem in simulating (or more precisely: in emulating) an amorphous computing system stems from the fact that such systems, in dependence on the input size, are capable to perform a potentially unbounded number of parallel opera-tions in constant time. This cannot be done by any uniform physical model of a known parallel universal computer with a constant number of processors. Perhaps the selfreproduction mobile embodied automata present the first step towards a truly universal computational model.