Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Probabilistic Interval Analysis of Unreliable Programs

Dibyendu Das, Soumyajit Dey

TL;DR

This work addresses static reliability analysis for programs running on unreliable hardware that exhibits transient faults. It extends abstract interpretation with a probabilistic concrete domain $\mathcal{L}$ and a probabilistic interval abstract domain $M$, linked by a Galois connection $(\alpha,\gamma)$, to safely approximate the strongest post-condition $sp$ with a computable $sp^\#$ over intervals. The authors formalize the domains, prove their lattice properties, and derive sound, monotonically increasing abstractions to compute probabilistic intervals for each program variable at every program point, using fixpoint iterations and widening for scalability. A prototype tool analyzes a C-like language, producing output intervals with associated probabilities, and demonstrates feasibility on small benchmarks (e.g., Collatz, GCD) while highlighting the trade-off between precision and performance. Overall, the approach provides a principled foundation for quantifying software reliability on unreliable hardware, enabling reliability-aware analysis and design in approximate computing and safety-critical contexts.

Abstract

Advancement of chip technology will make future computer chips faster. Power consumption of such chips shall also decrease. But this speed gain shall not come free of cost, there is going to be a trade-off between speed and efficiency, i.e accuracy of the computation. In order to achieve this extra speed we will simply have to let our computers make more mistakes in computations. Consequently, systems built with these type of chips will possess an innate unreliability lying within. Programs written for these systems will also have to incorporate this unreliability. Researchers have already started developing programming frameworks for unreliable architectures as such. In the present work, we use a restricted version of C-type languages to model the programs written for unreliable architectures. We propose a technique for statically analyzing codes written for these kind of architectures. Our technique, which primarily focuses on Interval/Range Analysis of this type of programs, uses the well established theory of abstract interpretation. While discussing unreliability of hardware, there comes scope of failure of the hardware components implicitly. There are two types of failure models, namely: 1) permanent failure model, where the hardware stops execution on failure and 2) transient failure model, where on failure, the hardware continues subsequent operations with wrong operand values. In this paper, we've only taken transient failure model into consideration. The goal of this analysis is to predict the probability with which a program variable assumes values from a given range at a given program point.

Probabilistic Interval Analysis of Unreliable Programs

TL;DR

This work addresses static reliability analysis for programs running on unreliable hardware that exhibits transient faults. It extends abstract interpretation with a probabilistic concrete domain and a probabilistic interval abstract domain , linked by a Galois connection , to safely approximate the strongest post-condition with a computable over intervals. The authors formalize the domains, prove their lattice properties, and derive sound, monotonically increasing abstractions to compute probabilistic intervals for each program variable at every program point, using fixpoint iterations and widening for scalability. A prototype tool analyzes a C-like language, producing output intervals with associated probabilities, and demonstrates feasibility on small benchmarks (e.g., Collatz, GCD) while highlighting the trade-off between precision and performance. Overall, the approach provides a principled foundation for quantifying software reliability on unreliable hardware, enabling reliability-aware analysis and design in approximate computing and safety-critical contexts.

Abstract

Advancement of chip technology will make future computer chips faster. Power consumption of such chips shall also decrease. But this speed gain shall not come free of cost, there is going to be a trade-off between speed and efficiency, i.e accuracy of the computation. In order to achieve this extra speed we will simply have to let our computers make more mistakes in computations. Consequently, systems built with these type of chips will possess an innate unreliability lying within. Programs written for these systems will also have to incorporate this unreliability. Researchers have already started developing programming frameworks for unreliable architectures as such. In the present work, we use a restricted version of C-type languages to model the programs written for unreliable architectures. We propose a technique for statically analyzing codes written for these kind of architectures. Our technique, which primarily focuses on Interval/Range Analysis of this type of programs, uses the well established theory of abstract interpretation. While discussing unreliability of hardware, there comes scope of failure of the hardware components implicitly. There are two types of failure models, namely: 1) permanent failure model, where the hardware stops execution on failure and 2) transient failure model, where on failure, the hardware continues subsequent operations with wrong operand values. In this paper, we've only taken transient failure model into consideration. The goal of this analysis is to predict the probability with which a program variable assumes values from a given range at a given program point.
Paper Structure (10 sections, 7 theorems, 25 equations, 7 figures, 1 table)

This paper contains 10 sections, 7 theorems, 25 equations, 7 figures, 1 table.

Table of Contents

  1. Introduction
  2. Interval Analysis of Unreliable Programs
  3. The Probabilistic Concrete Domain, $(\mathcal{L},\sqsubseteq_L)$
  4. Hasse Diagram of Lattice $(\mathcal{L},\ \sqsubseteq_L)$
  5. Strongest Post-Condition Function, $sp : \mathcal{L}^n\to\mathcal{L}^n$
  6. Fix point computation of concrete program states using $sp$
  7. The Probabilistic Interval Abstract Domain, $(M,\sqsubseteq_M)$
  8. Hasse Diagram of Lattice $(M,\ \sqsubseteq_M)$
  9. Galois Connection, $\left\langle L,\sqsubseteq_L\right\rangle \xrightleftharpoons[\gamma]{\alpha} \left\langle M,\sqsubseteq_M\right\rangle$
  10. Safe Approximation of Strongest Post-Condition Function, $sp$, in the Abstract Domain $M$

Key Result

Lemma 3.1

$(\mathcal{L},\ \sqsubseteq_L)$ is a poset.

Figures (7)

  • Figure 1: Example program
  • Figure 2: Frontal View of $(\mathcal{L},\sqsubseteq_L)$
  • Figure 3: Lateral View (skewed) of $(\mathcal{L},\sqsubseteq_L)$
  • Figure 4: Rear View of $(\mathcal{L},\sqsubseteq_L)$
  • Figure 5: 2D Projectional View of $(M,\sqsubseteq_M)$
  • ...and 2 more figures

Theorems & Definitions (27)

  • Definition 3.1
  • Definition 3.2
  • Lemma 3.1
  • proof
  • Lemma 3.2
  • proof
  • Example 3.3
  • Definition 3.3
  • Definition 3.4
  • Definition 4.1
  • ...and 17 more