1 of 8

​

Software (in-)Correctness Analysis

Lecture-8

Finish-up on Shared Memory Models

Project Suggestions

Briefly on Murphi, Rumur, ROMP

Then onto

Symbolic Execution, SMT, KLEE, CSeq (Lec 9,10)

​

Ganesh Gopalakrishnan

2 of 8

Recap

  • So far
    • BDD , classical automata
    • Promela, an interesting language
      • Passing channels as reply-channels is cool
        • can form networks of processes
          • ideas in Pi-calculus etc
      • In our case
        • P1 sends a blue reply-channel, P2 sends a green reply-channel
          • FIFO is bent on replying on the right channel color it picked up first…
    • Message-passing concurrency
      • MPI-like idioms
      • instead of chan p = [0] of byte, you can have
        • xs p = [0] of byte
          • a Channel Contract !!
  • Then LTL, Liveness, Fairness, and even failures that happen when weak-fairness is given (in current quiz/poll set)

​

3 of 8

Now

  • A look at shared memory
    • weak memory models
    • Some defns about
      • Acquire, Release, … and mutex protocols
    • Non-blocking data structures
  • Will verify using CSeq etc (later)
  • Murphi demos (today)
  • Next week : start with SMT, KLEE

4 of 8

Encoding things in logic

5 of 8

Encoding things in logic

6 of 8

Encoding things in logic

7 of 8

Video explaining projects + Chart

8 of 8

Today

  • Motivations for Java Concurrency and handling it correctly
  • Verifying for data-race freedom
    • A recent (2018) paper by us
      • https://pruners.github.io/pdf/08425238.pdf
  • Go through Assignment-3 making sure your reading-load on it is decreased
  • Demo Murphi, pointing out its features