A linked list cache coherence protocol: verifying the bottom layer

High performance and correctness are crucially important in hardware development. This paper discusses aspects of correctness of a linked list cache coherence protocol. The protocol is tailored to execute as many operations as possible in parallel, achieving speed and avoiding the memory bottleneck. This makes it hard to verify that the protocol is correct. In the paper, a bottom layer of the protocol is identified and it is shown how the correctness of this layer can be established