[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[tlaplus] simulating a crash in PlusCal

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).



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.