[tlaplus] simulating a crash in PlusCal

["'Michal Jaszczyk' via tlaplus" <tlaplus@xxxxxxxxxxxxxxxx>]

I'm writing a spec about a file system in PlusCal:

* my global variables represent various data structures, both in memory and on disk

* my processes represent various components of the system, internal threads, user threads etc.

In order to simulate a crash, I'd like to do the following:

* clear all data structures according to how the crash affects them (e.g. in-memory caches are emptied, but on-disk state remains)

* re-initialize affected data structures according to how the recovery procedure works

* reset affected processes to the beginning

Specifically I have a question about that last point:

1) Is it sufficient to simply reset the 'pc' variable to the first label of a process?

2) What about procedure call stacks? (I don't have procedures currently, but I might)

3) What about process local variables? (Currently they are always initialized before being used, so I don't rely on their initial values in the initial state).

Thanks,

M.

-- 
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/690307a1-b16b-485d-ac88-98e71e95deb3n%40googlegroups.com.