[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[tlaplus] the chapter on A Caching Memory in the book
- From: ns <nedsri1988@xxxxxxxxx>
- Date: Thu, 7 Oct 2021 12:44:55 -0700 (PDT)
- Ironport-hdrordr: A9a23:fuR0ba1ispCGb6NzVkd+0wqjBK8kLtp133Aq2lEZdPU1SL36qynApoV/6faZslgssRIb+exoRpPwI080nKQdieJ6AV7FZmjbUQCTQL2Kg7GO/9SZIULDytI=
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
- what does "state of the interface" (memInt) represent? And what are the operators Send and Reply actually doing?
At first I thought they were implemented by the memory but they are not.
- is InternalMemory supposed to a spec of what's labeled MEMORY in the figure?
- It seems to me that WriteThroughCache essentially just extends (in the object oriented sense) MemoryInterface apart from having to re-express Req and Rsp on account of TLA not making the Frame assumption. In what sense is it "implementing" Memory?
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.