1993 Canada / United States meta

An Investigation of the Therac-25 Accidents

Nancy Leveson and Clark Turner, 1993 — six patients dead or maimed by a radiation machine because the software had a race condition the manufacturer believed was impossible.

Between June 1985 and January 1987, the Therac-25 medical linear accelerator, manufactured by Atomic Energy of Canada Limited, delivered massive radiation overdoses to at least six patients. Three died from the overdoses; others were severely injured. Nancy Leveson and Clark Turner, at the University of California, Irvine, conducted the definitive post-mortem. The proximate cause was a race condition in the control software: a flag variable was incremented rather than set, occasionally overflowed to zero, and bypassed safety interlocks when an operator typed quickly enough to hit the timing window. The deeper cause was that AECL had removed the hardware interlocks present on the Therac-20 and trusted the software to enforce safety alone — without proof, without independent review, and without the discipline Hamilton had named. Leveson's investigation became required reading in every software-safety curriculum.

Cultural context · Canada / United States

Atomic Energy of Canada Limited was a Crown corporation — a government-owned company that designed and exported nuclear reactors and medical accelerators. In the mid-1980s the FDA's regulation of medical-device software was weak; the agency did not have the technical capacity to audit complex embedded systems. AECL marketed the Therac-25 as a fully software-controlled successor to the Therac-20 specifically because removing the hardware interlocks lowered the cost. When the first overdoses occurred, AECL initially blamed operator error and refused to acknowledge software defects. The industry-wide response — formal certification regimes for medical-device software, the IEC 62304 standard, FDA pre-market software review — was a direct legacy of these six patients.

In plain terms

The Therac-25 was a radiation therapy machine. Patients with cancer would lie on a table and the machine would deliver a precisely calibrated dose of radiation to a tumor. In low-energy mode it used an electron beam directly. In high-energy mode it used a stronger electron beam pointed at a metal target to produce X-rays — but the metal target had to be physically rotated into place, because if the high-energy beam hit a patient without the target it would deliver, instead of a therapeutic dose, an instant lethal dose. The earlier Therac-20 had a hardware interlock that physically prevented the machine from firing the high-energy beam when the target was not in place. The Therac-25 removed the hardware interlock and replaced it with a software check. AECL believed the software would be safe. They were wrong. The bug was small. The control software used a flag variable to track machine state. The variable was incremented on each setup pass. Most of the time this worked. But the variable was a single byte, and on roughly one pass in two hundred and fifty-six it overflowed back to zero — and zero meant "okay to fire." If an operator was experienced enough to type the setup commands faster than the machine could fully react, they could hit the timing window where the flag had overflowed but the target was not in place. The machine would fire. The patient would receive between fifty and a hundred times the prescribed dose. Six patients. Three deaths. And a generation of software safety engineers shaped by this case. The lesson is the one this book keeps returning to. Hoare's triples make safety provable. Hamilton's discipline makes safety routine. Skip both, and you get the Therac-25. The patients were not killed by an exotic flaw. They were killed by an integer overflow that any formal-methods discipline would have caught — that any proof obligation on the precondition "high-energy mode implies target in place" would have flagged before the machine ever shipped. Six patients. One race condition. The cost of skipping the discipline.