3 ms·

Are there tools out there that can prove semantic invariants in multi-threaded code? I don't understand how there can be automated tools around it at all becaus

Are there tools out there that can prove semantic invariants in multi-threaded code? I don't understand how there can be automated tools around it at all because how would that even be possible?

jeffreygoesto 3y ago
TLA+ comes to mind [0] https://www.learntla.com/index.html https://www.learntla.com/index.html
maxbond 3y ago
Rust comes to mind.
- redixhumayun 3y ago
  How would Rust solve this problem?
  - maxbond 3y ago
    All I meant was that it "proves semantic invariants in multi-threaded code," which proves the concept.
    - kaba0 3y ago
      No data races is just a very tiny subset of semantic invariants, though.
      - redixhumayun 3y ago
        I assumed what the poster above meant was that Rust can take care of more than just data races. Specifically Rust can solve the ABA problem somehow?
        maxbond 3y ago
        Rust won't solve the ABA problem, no. You'd be in unsafe Rust if you were writing something that could encounter the ABA problem. You wondered out loud how it was even possible to do that kind of analysis, and that's where my mind went. Evidently people think it's a bad take. That's as deep as it goes.
        infamouscow 3y ago
        The ABA problem is a false-positive execution of a CAS speculation on a shared memory location. It is very easy to create an ABA problem in safe Rust. Data race free sequential consistency, which Rust has, is almost completely orthogonal to the ABA problem. This is an area of active PLT research, we haven't come anywhere close to addressing the problem in the general case. I suspect we'll be seeing all kinds of bugs caused by a generation of programmers thinking everything has guard rails in Rust because "safety", so they can turn their brain off and not think. In reality, those promises of safety largely disappear when threads, files, signals, and networks are involved. At the end of the day, your programs run on computers which exist in the physical world. The abstractions are mostly isomorphic, but it's at the margins where the abstractions aren't isomorphic that all the interesting things happen.
        deleted 3y ago
        [deleted]
        maxbond 3y ago
        > The ABA problem is a false-positive execution of a CAS speculation on a shared memory location. In safe Rust, if I have a mutable reference to Foo, and Foo contains a shared reference to Bar, then no other thread has a mutable reference to Foo or Bar. So no other thread will make a CAS on my reference to Bar, or drop Bar and then allocate something at the same memory address, etc. You could have some higher level ABA problem I suppose, where you acquire a lock, read a value, give up the lock, and then make spurious assumptions about what happens while you've let the lock go. But that's obviously not what we're talking about if we're talking about CAS. (ETA: or if these were application level references, eg indices into a list.) If we're going to implement a lockfree data structure, we're going to need unsafe Rust to hand-roll interior mutability. Because we're going to be sharing mutable state. Which isn't allowed in safe Rust. Or am I mistaken?
kangda123 3y ago
There are model checkers such as nidhugg (C++), dscheck (ocaml). They take a test case and reach all possible terminal states by trying different interleavings. Crucially, they don’t have to try all interleavings to reach all terminal states, making the enumeration quite fast.

Are there tools out there that can prove semantic invariants in multi-threaded code? I don't understand how there can be automated tools around it at all because how would that even be possible?

jeffreygoesto 3y ago

TLA+ comes to mind [0] https://www.learntla.com/index.html https://www.learntla.com/index.html

maxbond 3y ago

Rust comes to mind.

redixhumayun 3y ago
How would Rust solve this problem?
- maxbond 3y ago
  All I meant was that it "proves semantic invariants in multi-threaded code," which proves the concept.
  - kaba0 3y ago
    No data races is just a very tiny subset of semantic invariants, though.
    - redixhumayun 3y ago
      I assumed what the poster above meant was that Rust can take care of more than just data races. Specifically Rust can solve the ABA problem somehow?
      - maxbond 3y ago
        Rust won't solve the ABA problem, no. You'd be in unsafe Rust if you were writing something that could encounter the ABA problem. You wondered out loud how it was even possible to do that kind of analysis, and that's where my mind went. Evidently people think it's a bad take. That's as deep as it goes.
        infamouscow 3y ago
        The ABA problem is a false-positive execution of a CAS speculation on a shared memory location. It is very easy to create an ABA problem in safe Rust. Data race free sequential consistency, which Rust has, is almost completely orthogonal to the ABA problem. This is an area of active PLT research, we haven't come anywhere close to addressing the problem in the general case. I suspect we'll be seeing all kinds of bugs caused by a generation of programmers thinking everything has guard rails in Rust because "safety", so they can turn their brain off and not think. In reality, those promises of safety largely disappear when threads, files, signals, and networks are involved. At the end of the day, your programs run on computers which exist in the physical world. The abstractions are mostly isomorphic, but it's at the margins where the abstractions aren't isomorphic that all the interesting things happen.
        deleted 3y ago
        [deleted]
        maxbond 3y ago
        > The ABA problem is a false-positive execution of a CAS speculation on a shared memory location. In safe Rust, if I have a mutable reference to Foo, and Foo contains a shared reference to Bar, then no other thread has a mutable reference to Foo or Bar. So no other thread will make a CAS on my reference to Bar, or drop Bar and then allocate something at the same memory address, etc. You could have some higher level ABA problem I suppose, where you acquire a lock, read a value, give up the lock, and then make spurious assumptions about what happens while you've let the lock go. But that's obviously not what we're talking about if we're talking about CAS. (ETA: or if these were application level references, eg indices into a list.) If we're going to implement a lockfree data structure, we're going to need unsafe Rust to hand-roll interior mutability. Because we're going to be sharing mutable state. Which isn't allowed in safe Rust. Or am I mistaken?

kangda123 3y ago

There are model checkers such as nidhugg (C++), dscheck (ocaml). They take a test case and reach all possible terminal states by trying different interleavings. Crucially, they don’t have to try all interleavings to reach all terminal states, making the enumeration quite fast.