Encode multiple paths in a thread as partial orders

These changes unify the treatment of inter-thread and intra-thread
memory accesses. At the core of this unification is the representation
of a structured program as a series-parallel graph. This graph induces a
partial order between events in a single thread. This ordering together
with the other axioms allow us to encode multiple execution paths
within a single thread of execution thereby generalizing multi-path
(i.e. CBMC-style) symbolic execution to concurrent programs. Further
work and optimizations on thread-local events, however, is required.