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

[tlaplus] the chapter on A Caching Memory in the book

hello I am trying to form a conceptual picture of how all the different memory related specs in Chapter 5 of Specifying Systems relate to each other. First off is MemoryInterface which I understand to be essentially the signature of the  interface over which the processor and memory communicate (the dashed box in the figure) . This has a variable memInt which represents the "state of the interface". Then comes the spec InternalMemory which makes use of the MemoryInterface (specifically the Send and Reply actions). This is wrapped inside a module called Memory to hide the internal vars. Finally there's WriteThroughCache which it says "implements the memory specification". My questions are


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/4fd0292c-8a33-48ee-a9d7-5fff8ce98df1n%40googlegroups.com.