Add Stack<T> API and fix LIFO order axiom

Consider the following two threads:

    T0   |  T1
---------+-------
 push(A) | pop()
 push(B) | pop()

The unfixed stack partial order axiom required the pops to respect
the usual LIFO ordering even though the second push in T0 might not
globally happen before the first pop in T1.