class Client {
  method Main(d: Data)
    requires d != null
  {
    var a := new AssociationList
    call a.Init()
    call a.Add(5, d)
    call a.Add(10, d)
    var t: Data
    call t := a.Get(10)
  }
}

class AssociationList {
  var head: Node  // sentinel
  invariant rd(head) && head != null
  invariant rd(mu) && rd(head.mu) && this << head

  method Init()
    requires acc(head) && acc(mu) && mu == lockbottom
    ensures acc(mu) && waitlevel << this
  {
    head := new Node
    head.next := null
    share head
    share this between waitlevel and head
  }

  method Add(key: int, value: Data)
    requires value != null
    requires rd(mu) && waitlevel << this
    ensures rd(mu)
  {
    acquire this
    var p: Node := head
    acquire p
    release this

    var n := new Node
    n.key := key
    n.value := value
    n.next := p.next
    p.next := n
    share n between p and n.next
    release p
  }

  method Get(key: int) returns (d: Data)
    requires rd(mu) && waitlevel << this
    ensures rd(mu)
  {
    d := null
    acquire this
    var p: Node := head
    acquire p
    release this

    if (p.next != null) {
      acquire p.next
      if (p.next.key == key) {
        d := p.next.value
      } else {
        var done := false
        while (!done)
          // invariant:  holds p and p.next
          invariant p != null && rd(p.key) && rd(p.value) && acc(p.next) && acc(p.mu,50) && p.next != null
          invariant acc(p.next.mu) && p << p.next
          invariant rd(p.next.key) && rd(p.next.value) && acc(p.next.next)
          invariant p.next.next != null ==>
              acc(p.next.next.mu,50) && p.next << p.next.next
          invariant holds(p) && holds(p.next) && waitlevel == p.next.mu
          invariant p.next.next != null ==> waitlevel << p.next.next
          lockchange p, p.next.next
        {
          if (p.next.next == null) {
            done := true  // key not present
          } else {
            acquire p.next.next
            if (p.next.next.key == key) {
              done := true  // key is present
              d := p.next.next.value
              // move p.next.next closer to the head by one step

              var t: Node := p.next
              p.next := t.next
              t.next := p.next.next
              p.next.next := t
              reorder t between p.next and t.next
              release t
            } else {
              var t: Node := p
              p := p.next
              release t
            }
          }
        }
      }
      release p.next
    }
    release p
  }
}

class Data { }

class Node
{
  var key: int
  var value: Data
  var next: Node
  invariant rd(key) && rd(value) && acc(next) && acc(mu,50)
  invariant next != null ==> acc(next.mu,50) && this << next
}