1 of 10

​

Software (in-)Correctness Analysis

Lecture-3

​

Ganesh Gopalakrishnan

2 of 10

Today's Topic: Concurrency Verification

  • Bugs can fester for a decade!

It turned out to be a very simple problem. Like so many other aspects of Photoshop, it had to do with the fact that the app was written first for the Macintosh and then moved over to Windows. On the Macintosh, the set file position call is atomic—a single call—whereas on Windows, it's a pair of calls. The person who put that in there didn't think about the fact that the pair of calls has to be made atomic whenever you're sharing the file position across threads.

COLE Now, of course, you can look back and say that's obvious.

WILLIAMS In fact, the person who originally put that bug in the code was walking down the hallway one of the many times we set off looking for that thing, smacked his forehead, and realized what the problem was—10 years after the fact.

​

3 of 10

Concurrency Verification Challenges

  • Interleavings go fast
    • N threads of K steps each have a total of (N.K)! / (K!)^N interleavings
    • N=5 and K=10 has over 48 * 10^30 interleavings
  • Atomicity is often non-apparent
  • Weak memory model effects are often misunderstood
    • Compiler
    • Hardware
  • Speeds are skewed by ``surrounding code'' that takes time and hence prevents many schedules from being present
  • Many kinds of threading and many "inner notions"
    • Threads and tasks : OpenMP
    • Threads and Goroutines : Go
    • Others that border on message-passing but realized using shared memory
      • There is room to grow in all of these
        • Data Race Checking seems to be an actionable FV path with recognized value!

4 of 10

What I'll do / emphasize

  • Introduce you to the notions
    • People are groping for ways to formally express certain things
      • e.g. producer/consumer patterns in C++ threading and patterns
      • e.g. release/acquire and others
      • May not enter the Dist Systems space
        • its own notions
      • Rather I may stay inside the "shared memory space"
        • plenty to learn
  • Try and introduce ways to model and solve these notions
    • e.g. defining weak-memory consistency using Alloy
    • e.g. modeling it using Promela
    • e.g. modeling it in the Cseq tool and verifying
    • e.g. finding litmus tests that expose bugs in this space
  • With that in mind, I now begin talking about
    • PThread programs
      • Can we test them?
    • How to model/verify using CSeq (for later; now a brief demo)
      • You may face tool limitations
    • How to model/verify using Promela/SPIN
      • This is affordable wrt verif time investments
  • The industry has better FV tools!
    • If I show FV principles + small examples, you still have the excitement
      • The industry will still hire you if you can think in this space and use tools on small issues
        • e.g. anecdotally I've seen people "go after" the Herlihy / Shavit book examples
          • This is enough to get hired if you can solve those!
    • If I show medium/hard problems and show FV fails , you won't use it again

5 of 10

A PThread Program: Does it bomb?

6 of 10

A PThread Program

modeled

for exploration

by the

LazyCseq tool (later):

  • How to allocate bounds (loop unroll and number of context-switches or rounds)
  • Shows how to build tools that "last"
    • source2source done using Python seems better!

7 of 10

A PThread Program

modeled in Promela

for exploration

by SPIN

8 of 10

A PThread Program

modeled in Promela

for exploration

by SPIN: Contrast of reality vs modeling

9 of 10

A PThread Program

modeled in Promela

for exploration

by SPIN: Contrast of reality vs modeling

  • Once you learn Promela/SPIN well, you can model + analyze huge systems in it!
    • See its use in this book by Paul E. McKenney (rdrop…)
      • Models real OS constructs in it
        • Gets mileage
          • The most practical FV tool one can pick up in a class like this!
            • Finally, the tool is helping you think …
              • Lamport's TLA+ message + talks around it!
    • See its use in QThreads cancellation in the SC correctness workshop (ask me)

10 of 10

Demos, followed by study of Promela

  • Demo of PThread execution
    • hit/miss bug hunting
  • Demo of CSeq-based verification
    • Demo now; will study soon
  • Demo of Promela/SPIN verification
    • The rest of this week
      • ManyTinyPromelaExs.pdf will be the slide-deck we shall study