• Bug discovered: pure functions are incorrectly translated into Boogie.
• Problem: access to local variables of other threads is in VCC not possible on the specification level. Solution: pack locals into structures which the current thread possesses.
• Possible unsoundness:
  _(requires \wrapped(&inst))
_(requires \wrapped(&local_sense))
  leads to succeeding
  _(assert \false).
  Solution: do not use shared file-scope variables.
• Apparently, \me is not a \thread, so there is no way to distinguish the current thread from the others. Bug reported.
• File-scope statically default-initialized variables are not supported. Not really disturbing, but bug reported.
• We can't prove that pc[\me] remains unchanged between the actions of the verified thread.
  Trying out: expose all local state into a shared structure LocalData and maintain a map of such local structures.
  Subproblem: Complicated assignments like p_inst->ld[\me].local_sense^=1 can't be parsed. Solution to the subproblem: use temporary variables.
  Subproblem: substructures can't be owned. Trying out: declare pointers to substructures.
• Problem solved: Developers have provided a bunch of undocumented features that allow expressing ownership over the local state. New problem: expressing nontrivial features of the shared data structure that require recursive predicates fails.
• Solution to the previous problem: recursive predicate abandoned, since VCC provides no checking support for them and using Boogie-HOL is "probably not going to work". Instead encode "the number of threads before the decrement = count" as "exactly the threads with thread ID < count are before the decrement" and swap the thread IDs dynamically. Requires maintaining a bijection.
• Problem: annotations are huge. Simplification of the bijection as suggested by the developpers does not work. That's why: the buggy construct "depends" was used.
  Solution: use "approves" instead of "depends". Now the annotations of the simplest barrier core are simpler.
• The barrier gets verified in 4.4 s. Suggestions of the developpers are partially implemented. Code was slightly simplified and verifies now in 3.752857 s.
• Then, we made the code got textually smaller and easier to understand. The time to verify is 4.73 s.
• Finally, it turned out that we don't need the abstract location WaitPL. Got rid of it. The time to verify is now 2.92 s on an Intel 2.4 GHz Intel® CPU with 8 GB RAM.
• The VCC team has changed bool to \bool, but also improved threorem proving. As a result, the check myId < s->count is no more needed. The time to verify is now 3.427 s on an Intel® Core™ 2 DUO L7500 CPU clocked at 1.6 GHz with 1.5 GB RAM clocked at 533 MHz.