1. 20
  1.  

  2. 2

    In this specific case, I believe the model only fails if you pick the constants appropriately: spawn more goroutines than buffered slots. But that’s basically the bug in the first place, so it leaves me with the feeling that it helps you find the bug if you know what the bug is already. That said, I can see how writing the model might help focus the author on the choice of constants and help them discover the bug.

    I’d be interested to hear the authors thoughts on that. Does that feeling sound fair? Are there tools that would find choices for the constants that fail for you?

    1. 6

      In this case I modeled it to closely match the code, but normally you’d design the spec so that it “sweeps” through a space of possible initial values. It’d look something like

      variables
        Routines \in {1..x: x \in 1..MaxRoutines};
        NumTokens \in 1..MaxTokens;
        channels = [limitCh |-> 0, found |-> {}];
        buffered = [limitCh |-> NumTokens];
        initialized = [w \in Routines |-> FALSE];
      

      Then it would try 1 routine and 1 token, 1 routine and 2 tokens, etc.

      1. 1

        Here I believe the NumRoutines constant exists to ensure the model is bounded– TLC will check every number of potential goroutines from 1 to whatever NumRoutines ends up being. In addition, there are actually only two buffered channels to begin with (“limitCh” and “found”). As long as NumRoutines >= 3, then, TLA will find this issue.

        In my experience writing the model helps you better understand the problem and thus pick appropriate constants (as you mentioned). But even if it didn’t, it wouldn’t be unreasonable with this spec to plug in 10 for NumRoutines and see what happens.

        With TLA+ models I find that I wind up with an emotion similar to writing untested code: if it 100% works the first time I get immediately suspicious and start poking at things until they break as a means to convince myself it was actually working.

        1. 1

          In addition, there are actually only two buffered channels to begin with (“limitCh” and “found”). As long as NumRoutines >= 3, then, TLA will find this issue.

          I disagree. Found is unbuffered, and limitCh is buffered. I believe it will only find the bug if NumRoutines >= the buffer size of limitCh.

          1. 1

            Oh beans, in my pre-meeting rush I misread the spec. Which is definitely a separate problem!

            So it looks like limitCh has a buffer the size of NumTokens and you’d want to ensure you pick NumRoutines > NumTokens during one of the runs, right? I’m not sure there’s a tool that checks your work there.

          2. 1

            Here I believe the NumRoutines constant exists to ensure the model is bounded– TLC will check every number of potential goroutines from 1 to whatever NumRoutines ends up being. In addition, there are actually only two buffered channels to begin with (“limitCh” and “found”). As long as NumRoutines >= 3, then, TLA will find this issue.

            While that’s best practice, here I fixed the number of routines at NumRoutines for simplicity. It will find also find a bug with 2 routines and 1 token.