REPAIR: Control Flow Protection based on Register Pairing Updates for SW-Implemented HW Fault Tolerance

Safety-critical embedded systems may either use specialized hardware or rely on Software-Implemented Hardware Fault Tolerance (SIHFT) to meet soft error resilience requirements. SIHFT has the advantage that it can be used with low-cost, off-the-shelf components such as standard Micro-Controller Units. For this, SIHFT methods apply redundancy in software computation and special checker codes to detect transient errors, so called soft errors, that either corrupt the data flow or the control flow of the software and may lead to Silent Data Corruption (SDC). So far, this is done by applying separate SIHFT methods for the data and control flow protection, which leads to large overheads in computation time. This work in contrast presents REPAIR, a method that exploits the checks of the SIHFT data flow protection to also detect control flow errors as well, thereby, yielding higher SDC resilience with less computational overhead. For this, the data flow protection methods entail duplicating the computation with subsequent checks placed strategically throughout the program. These checks assure that the two redundant computation paths, which work on two different parts of the register file, yield the same result. By updating the pairing between the registers used in the primary computation path and the registers in the duplicated computation path using the REPAIR method, these checks also fail with high coverage when a control flow error, which leads to an illegal jumps, occurs. Extensive RTL fault injection simulations are carried out to accurately quantify soft error resilience while evaluating Mibench programs along with an embedded case-study running on an OpenRISC processor. Our method performs slightly better on average in terms of soft error resilience compared to the best state-of-the-art method but requiring significantly lower overheads. These results show that REPAIR is a valuable addition to the set of known SIHFT methods.

Self-Verifying Pushdown and Queue Automata

We study the computational and descriptional complexity of self-verifying pushdown automata (SVPDA) and self-verifying realtime queue automata (SVRQA). A self-verifying automaton is a nondeterministic device whose nondeterminism is symmetric in the following sense. Each computation path can give one of the answers yes, no, or do not know. For every input word, at least one computation path must give either the answer yes or no, and the answers given must not be contradictory. We show that SVPDA and SVRQA are automata characterizations of so-called complementation kernels, that is, context-free or realtime nondeterministic queue automaton languages whose complement is also context free or accepted by a realtime nondeterministic queue automaton. So, the families of languages accepted by SVPDA and SVRQA are strictly between the families of deterministic and nondeterministic languages. Closure properties and various decidability problems are considered. For example, it is shown that it is not semidecidable whether a given SVPDA or SVRQA can be made self-verifying. Moreover, we study descriptional complexity aspects of these machines. It turns out that the size trade-offs between nondeterministic and self-verifying as well as between self-verifying and deterministic automata are non-recursive. That is, one can choose an arbitrarily large recursive function f, but the gain in economy of description eventually exceeds f when changing from the former system to the latter.

Iterative arrays with self-verifying communication cell

We study the computational capacity of self-verifying iterative arrays ($${\text {SVIA}}$$ SVIA ). A self-verifying device is a nondeterministic device whose nondeterminism is symmetric in the following sense. Each computation path can give one of the answers yes, no, or do not know. For every input word, at least one computation path must give either the answer yes or no, and the answers given must not be contradictory. It turns out that, for any time-computable time complexity, the family of languages accepted by $${\text {SVIA}}$$ SVIA s is a characterization of the so-called complementation kernel of nondeterministic iterative array languages, that is, languages accepted by such devices whose complementation is also accepted by such devices. $${\text {SVIA}}$$ SVIA s can be sped-up by any constant multiplicative factor as long as the result does not fall below realtime. We show that even realtime $${\text {SVIA}}$$ SVIA are as powerful as lineartime self-verifying cellular automata and vice versa. So they are strictly more powerful than the deterministic devices. Closure properties and various decidability problems are considered.

Testing a new idea to solve the P = NP problem with mathematical induction

Background. P and NP are two classes (sets) of languages in Computer Science. An open problem is whether P = NP. This paper tests a new idea to compare the two language sets and attempts to prove that these two language sets consist of same languages by elementary mathematical methods and basic knowledge of Turing machine. Methods. By introducing a filter function C(M,w) that is the number of configurations which have more than one children (nondeterministic moves) in the shortest accept computation path of a nondeterministic Turing machine M for input w, for any language L(M) ∈ NP, we can define a series of its subsets, Li(M) = {w | w ∈ L(M) ∧ C(M,w) ≤ i}, and a series of the subsets of NP as Li = {Li(M) | ∀M ∙ L(M) ∈ NP}. The nondeterministic multi-tape Turing machine is used to bridge two language sets Li and Li+1, by simulating the (i+1)-th nondeterministic move deterministically in multiple work tapes, to reduce one (the last) nondeterministic move. Results. The main result is that, with the above methods, the language set Li+1, which seems more powerful, can be proved to be a subset of Li. This result collapses Li ⊆ P for all i ∈ N. With NP = ⋃i∈NLi, it is clear that NP ⊆ P. Because by definition P ⊆ NP, we have P = NP. Discussion. There can be other ways to define the subsets Li and prove the same result. The result can be extended to cover any sets of time functions C, if ∀f ∙ f ∈ C ⇒ f2 ∈ C, then DTIME(C) = NTIME(C). This paper does not show any ways to find a solution in P for the problem known in NP.

Testing a new idea to solve the P = NP problem with mathematical induction

Background. P and NP are two classes (sets) of languages in Computer Science. An open problem is whether P = NP. This paper tests a new idea to compare the two language sets and attempts to prove that these two language sets consist of same languages by elementary mathematical methods and basic knowledge of Turing machine. Methods. By introducing a filter function C(M,w) that is the number of configurations which have more than one children (nondeterministic moves) in the shortest accept computation path of a nondeterministic Turing machine M for input w, for any language L(M) ∈ NP, we can define a series of its subsets, Li(M) = {w | w ∈ L(M) ∧ C(M,w) ≤ i}, and a series of the subsets of NP as Li = {Li(M) | ∀M ∙ L(M) ∈ NP}. The nondeterministic multi-tape Turing machine is used to bridge two language sets Li and Li+1, by simulating the (i+1)-th nondeterministic move deterministically in multiple work tapes, to reduce one (the last) nondeterministic move. Results. The main result is that, with the above methods, the language set Li+1, which seems more powerful, can be proved to be a subset of Li. This result collapses Li ⊆ P for all i ∈ N. With NP = ⋃i∈NLi, it is clear that NP ⊆ P. Because by definition P ⊆ NP, we have P = NP. Discussion. There can be other ways to define the subsets Li and prove the same result. The result can be extended to cover any sets of time functions C, if ∀f ∙ f ∈ C ⇒ f2 ∈ C, then DTIME(C) = NTIME(C). This paper does not show any ways to find a solution in P for the problem known in NP.

The linear-hyper-branching spectrum of temporal logics

The family of temporal logics has recently been extended with logics for the specification of hyperproperties, such as noninterference or observational determinism. Hyperproperties relate multiple computation paths of a system by requiring that they satisfy a certain relationship, such as an identical valuation of the low-security outputs. Unlike classic temporal logics like LTL or CTL*, which refer to one computation path at a time, temporal logics for hyperproperties like HyperLTL and HyperCTL* can express such relationships by explicitly quantifying over multiple computation paths simultaneously. In this paper, we study the extended spectrum of temporal logics by relating the new logics to the linear-branching spectrum of process equivalences.

Introductory Quantum Algorithms

In this chapter we will describe some of the early quantum algorithms. These algorithms are simple and illustrate the main ingredients behind the more useful and powerful quantum algorithms we describe in the subsequent chapters. Since quantum algorithms share some features with classical probabilistic algorithms, we will start with a comparison of the two algorithmic paradigms. Classical probabilistic algorithms were introduced in Chapter 1. In this section we will see how quantum computation can be viewed as a generalization of probabilistic computation. We begin by considering a simple probabilistic computation. Figure 6.1 illustrates the first two steps of such a computation on a register that can be in one of the four states, labelled by the integers 0, 1, 2, and 3. Initially the register is in the state 0. After the first step of the computation, the register is in the state j with probability p0,j . For example, the probability that the computation is in state 2 after the first step is p0,2. In the second step of the computation, the register goes from state j to state k with probability qj,k. For example, in the second step the computation proceeds from state 2 to state 3 with probability q2,3. Suppose we want to find the total probability that the computation ends up in state 3 after the second step. This is calculated by first determining the probability associated with each computation ‘path’ that could end up at the state 3, and then by adding the probabilities for all such paths. There are four computation paths that can leave the computation in state 3 after the first step. The computation can proceed from state 0 to state j and then from state j to state 3, for any of the four j ∊ {0, 1, 2, 3}. The probability associated with any one of these paths is obtained by multiplying the probability p0,j of the transition from state 0 to state j, with the probability qj,3 of the transition from state j to state 3.

HOPLA--A Higher-Order Process Language

A small but powerful language for higher-order nondeterministic processes is introduced. Its roots in a linear domain theory for concurrency are sketched though for the most part it lends itself to a more operational account. The language can be viewed as an extension of the lambda calculus with a ``prefixed sum'', in which types express the form of computation path of which a process is capable. Its operational semantics, bisimulation, congruence properties and expressive power are explored; in particular, it is shown how it can directly encode process languages such as CCS, CCS with process passing, and mobile ambients with public names.

THE EFFECT OF THE NUMBER OF SUCCESSFUL PATHS IN A BÜCHI TREE AUTOMATON

We modify an acceptance condition of Büchi automaton on infinite trees: rather than to require that each computation path is successful, we impose various restrictions on the number of successful paths in a run of the automaton on a tree. All these modifications alter the recognizing power of Büchi automata. We examine the classes induced by the acceptance conditions that require ≤α, ≥α, =α successful paths, where α is a cardinal number. It turns out that, except for some trivial cases, the “≤” classes are incomparable with the class Bü of Büchi acceptable tree languages, while the classes “≥” are strictly included in Bü.