change the name of "state" to "memory"
add definition for tid
add the definition for Lock
add definition for Write Buffer
mimicking the usage of Record, state is now a "Record"
simply finish the definition for new "state", next is to update old a/b/c definitions
now write buffer appends writes to the end (rather than insert in the head)
clear some old comments and TODOs
update unlock()
add some useful tactics to XLib.v
determine the form of buffer and threads, next is semantics
rewrite the aeval() and beval()
change the representation again.. now ready to write down small-step semantics
add some notes, done today
add the relation definition in XLib.v, for smallstep semantics
add the smallstep semantics for AE & BE
add the strong_progress theorem for AE/BE's smallstep semantics
add test cases for write buffers
add most of smallstep semantics, but there are flaws to resolve
plan to have a set tid containing all current tids; put testing functions in a separate module