Verifying quantitative reliability of programs that execute on unreliable hardware

Emerging high-performance architectures are anticipated to contain unreliable components that may exhibit soft errors, which silently corrupt the results of computations. Full de-tection and masking of soft errors is challenging, expensive, and, for some applications, unnecessary. For example, ap-proximate computing applications (such as multimedia pro-cessing, machine learning, and big data analytics) can often naturally tolerate soft errors. We present Rely, a programming language that enables developers to reason about the quantitative reliability of an application – namely, the probability that it produces the correct result when executed on unreliable hardware. Rely allows developers to specify the reliability requirements for each value that a function produces. We present a static quantitative reliability analysis that verifies quantitative requirements on the reliability of an ap-plication, enabling a developer to perform sound and verified reliability engineering. The analysis takes a Rely program with a reliability specification and a hardware specification that characterizes the reliability of the underlying hardware components and verifies that the program satisfies its relia-bility specification when executed on the underlying unreli-able hardware platform. We demonstrate the application of quantitative reliability analysis on six computations imple-mented in Rely