|
|
|
|
|
by pron
3324 days ago
|
|
You just define it :) TLA+ doesn't have a built-in memory model, nor any concept of memory whatsoever. You define your constructs at the level of detail you think is important. Weak memory can be defined using a CPU-local memory that is occasionally reconciled with RAM or other core-local memory. |
|