model: generate UNINIT actions as new atomic operations form

model: generate UNINIT actions as new atomic operations form

The first time an atomic variable is accessed, we need to add an
appropriate UNINIT action to the ModelChecker data structures. We assign
these ModelActions to the special model-checker thread (Thread 0). Note
that these actions will *not* appear in the NodeStack and will not be
explored in check_current_action, etc.