5 ms·

I'm curious how OP would prevent the Therac incident through type systems... Key quote: "Previous models had hardware interlocks in place to prevent this, but

by blub 9y ago

I'm curious how OP would prevent the Therac incident through type systems... Key quote: "Previous models had hardware interlocks in place to prevent this, but Therac-25 had removed them, depending instead on software interlocks for safety." Or even better how type systems could work around data integrity errors in RAM without ECC.

kazinator 9y ago
Maybe I'm recalling things wrong (the incident is very old and I last read the details before some HN-ers here were born), but at the heart of the Therac-25 issue was flaky code, written in a language without any type enforcement (assembly language). What's worse, the code was juggling concurrent events with interrupts and whatnot and was laden with race conditions (probably a phrase not even in the developer's vocabulary).
- blub 9y ago
  Pages 42-end of Leveson's report explain the fixes put in place and the contributing causes. Software bugs are a contributing factor, but the report warns against focusing myopically on the bugs.
SomeStupidPoint 9y ago
> Or even better how type systems could work around data integrity errors in RAM without ECC. You realize that you can do ECC in software too, right? You just need the statistical bound on a double fault to be similar to that of the hardware case. Type systems can be used to do this by defining an interface for the data, letting you swap between normal datatypes and ECC ones seamlessly. (And in practice, you only need to define the base operators for your new type.) You can do this with ducktyping ECC versions of objects in say... Python. But the type system helps ensure that you've built the full set of components necessary and it properly links. You have to do this with ad hoc IDE tools in Python. Similarly.... > The defect was as follows: a one-byte counter in a testing routine frequently overflowed; if an operator provided manual input to the machine at the precise moment that this counter overflowed, the interlock would fail. That actually sounds like exactly the situation that a type system would be used to prevent -- partly because from a type theoretic perspective, that whole situation sounds like an obvious defect. Further, the result was because of an obscure combination of key strokes that went untested. The use of total functions (enforced by the type system) lets you verify (by computer) that no combination of input can transition to a bad state. So... Did you intentionally pick two cases where type systems are the obvious solution to the problem?
- ec109685 9y ago
  What stops your program data from being modified or tampwered with without ECC ram, bypassing your checks?
  - SomeStupidPoint 9y ago
    I'm not sure I understand your question, but the one that most pertains to ECC would be preventing corruption of the routine performing the checks -- It varies greatly by the method you use to ECC in software, since they all feature different mechanisms. In the case of the one I had in mind, the kernel is relatively small (so errors are unlikely), and once loaded, it's stable against bit errors. There are probably better answers, I'm not an expert on software ECC. (Tampering is a different issue -- if they can tamper with the program, ECC won't save you from them writing garbage to memory. So that a hack which can write memory can bypass memory safety isn't really interesting.)
    - ec109685 9y ago
      I meant tampering via a side channel attack (e.g. forcing a bit flip that ecc would protect). It doesn’t matter if your data types have referential integrity if a hacker could disable that protection. What I am arguing against is saying a typesafe language obviates the need for ecc memory.
      - SomeStupidPoint 9y ago
        > What I am arguing against is saying a typesafe language obviates the need for ecc memory. Which isn't what anyone said: I claimed you can do ECC in software and that type systems assist with that by making a clean interface and verifying the full implementation. (Since ECC is really just a lift of normal functions.) There's little difference between using 9 bits in hardware and 9 bits in software, except that you need to cleanly load your ECC code onto CPU cache and you're using CPU instructions per byte loaded. The reason we do ECC in hardware is efficiency on an operation we're doing on literally every byte. Lots of systems, eg harddrives, use ECC in their actual formats too, because you can do more complex ECC at the software level and not merely the extra bit. Sometimes, this software ECC is more efficient than hardware based ECC would be, because we're okay with less than 12.5% redundancy as long as we can still correct the errors we expect to find.
dkersten 9y ago
So because a tool can't prevent all possible faults or problems, that tool isn't worthwhile? I see it like this: we have a number of different tools to minimise problems (various types of testing, theorem provers, type systems etc). Non of them catch every problem and many of the tools overlap in the types of problems they do catch, but if you use many of these techniques together, then you minimise the surface area of issues that can slip through. Very few things, in computers or "real life" are completely fool proof, but that doesn't mean that they are not worthwhile. That's a call that must be made on a case by case basis to weigh up the risk of faults, the damage done if a fault does occur, the cost of preventing said faults, your budget and time available etc...
- blub 9y ago
  OP said "Type systems to me seem to be (I'm not exaggerating) the answer to all software reliability problems (barring social ones)." Pay attention, please!
  - red75prime 9y ago
    OP hasn't said that it's the answer to the hardware problems as well.
    - blub 9y ago
      One needs to consider the safety of the system as a whole in order to build a safe system. Leaving aside social problems for instance is a bit like saying that one can build perfect software, with the small issue that it can't be used by humans. Leaving aside hardware is even more suspicious, because the two are inseparable in a system.
- deleted 9y ago
  [deleted]
deleted 9y ago
[deleted]
wyager 9y ago
Sounds like the Therac incident was caused by a concurrency error. Type systems can prevent this via type-level ownership systems (a la Rust) or safe concurrency types (a la Haskell’s STM).
- deleted 9y ago
  [deleted]

by blub 9y ago

kazinator 9y ago

Maybe I'm recalling things wrong (the incident is very old and I last read the details before some HN-ers here were born), but at the heart of the Therac-25 issue was flaky code, written in a language without any type enforcement (assembly language). What's worse, the code was juggling concurrent events with interrupts and whatnot and was laden with race conditions (probably a phrase not even in the developer's vocabulary).

blub 9y ago
Pages 42-end of Leveson's report explain the fixes put in place and the contributing causes. Software bugs are a contributing factor, but the report warns against focusing myopically on the bugs.

SomeStupidPoint 9y ago

> Or even better how type systems could work around data integrity errors in RAM without ECC. You realize that you can do ECC in software too, right? You just need the statistical bound on a double fault to be similar to that of the hardware case. Type systems can be used to do this by defining an interface for the data, letting you swap between normal datatypes and ECC ones seamlessly. (And in practice, you only need to define the base operators for your new type.) You can do this with ducktyping ECC versions of objects in say... Python. But the type system helps ensure that you've built the full set of components necessary and it properly links. You have to do this with ad hoc IDE tools in Python. Similarly.... > The defect was as follows: a one-byte counter in a testing routine frequently overflowed; if an operator provided manual input to the machine at the precise moment that this counter overflowed, the interlock would fail. That actually sounds like exactly the situation that a type system would be used to prevent -- partly because from a type theoretic perspective, that whole situation sounds like an obvious defect. Further, the result was because of an obscure combination of key strokes that went untested. The use of total functions (enforced by the type system) lets you verify (by computer) that no combination of input can transition to a bad state. So... Did you intentionally pick two cases where type systems are the obvious solution to the problem?

ec109685 9y ago
What stops your program data from being modified or tampwered with without ECC ram, bypassing your checks?
- SomeStupidPoint 9y ago
  I'm not sure I understand your question, but the one that most pertains to ECC would be preventing corruption of the routine performing the checks -- It varies greatly by the method you use to ECC in software, since they all feature different mechanisms. In the case of the one I had in mind, the kernel is relatively small (so errors are unlikely), and once loaded, it's stable against bit errors. There are probably better answers, I'm not an expert on software ECC. (Tampering is a different issue -- if they can tamper with the program, ECC won't save you from them writing garbage to memory. So that a hack which can write memory can bypass memory safety isn't really interesting.)
  - ec109685 9y ago
    I meant tampering via a side channel attack (e.g. forcing a bit flip that ecc would protect). It doesn’t matter if your data types have referential integrity if a hacker could disable that protection. What I am arguing against is saying a typesafe language obviates the need for ecc memory.
    - SomeStupidPoint 9y ago
      > What I am arguing against is saying a typesafe language obviates the need for ecc memory. Which isn't what anyone said: I claimed you can do ECC in software and that type systems assist with that by making a clean interface and verifying the full implementation. (Since ECC is really just a lift of normal functions.) There's little difference between using 9 bits in hardware and 9 bits in software, except that you need to cleanly load your ECC code onto CPU cache and you're using CPU instructions per byte loaded. The reason we do ECC in hardware is efficiency on an operation we're doing on literally every byte. Lots of systems, eg harddrives, use ECC in their actual formats too, because you can do more complex ECC at the software level and not merely the extra bit. Sometimes, this software ECC is more efficient than hardware based ECC would be, because we're okay with less than 12.5% redundancy as long as we can still correct the errors we expect to find.

dkersten 9y ago

So because a tool can't prevent all possible faults or problems, that tool isn't worthwhile? I see it like this: we have a number of different tools to minimise problems (various types of testing, theorem provers, type systems etc). Non of them catch every problem and many of the tools overlap in the types of problems they do catch, but if you use many of these techniques together, then you minimise the surface area of issues that can slip through. Very few things, in computers or "real life" are completely fool proof, but that doesn't mean that they are not worthwhile. That's a call that must be made on a case by case basis to weigh up the risk of faults, the damage done if a fault does occur, the cost of preventing said faults, your budget and time available etc...

blub 9y ago
OP said "Type systems to me seem to be (I'm not exaggerating) the answer to all software reliability problems (barring social ones)." Pay attention, please!
- red75prime 9y ago
  OP hasn't said that it's the answer to the hardware problems as well.
  - blub 9y ago
    One needs to consider the safety of the system as a whole in order to build a safe system. Leaving aside social problems for instance is a bit like saying that one can build perfect software, with the small issue that it can't be used by humans. Leaving aside hardware is even more suspicious, because the two are inseparable in a system.
deleted 9y ago
[deleted]

deleted 9y ago

[deleted]

wyager 9y ago

Sounds like the Therac incident was caused by a concurrency error. Type systems can prevent this via type-level ownership systems (a la Rust) or safe concurrency types (a la Haskell’s STM).

deleted 9y ago
[deleted]