model: add write-to-promise edges

model: add write-to-promise edges

Assume that any time a promise exists, is compatible with a store, and
is exclusive to the same thread as the store, that it is mod-ordered
after that store. This should never produce cycles, until we decide to
begin satisfying promises. At that point, if there's a cycle, then we
must either merge nodes (i.e., the store must satisfy that promise) or
else we discard the execution for the moment and perform the
satisfaction at a later point in the search space.