Share on Facebook Tweet on Twitter Share on LinkedIn Share by email
The Beehive Ring and Multiring Lock Protocols

Thomas L. Rodeheffer


Beehive is an experimental many-core computer implemented on a single FPGA. The system includes a number of RISC cores that are connected to each other and to main memory using a token ring interconnect. Among other things, the token ring is used to maintain a set of global hardware locks using a ring lock protocol. A multiring extension of the Beehive token ring has been proposed for which a more complicated multiring lock protocol is required.

This paper describes the ring lock protocol and the multiring lock protocol, presents correctness proofs, and discusses the results of checking their formal specifications using the TLC model checker. The formal specifications are listed in appendices.


Publication typeTechReport
PublisherMicrosoft Research
> Publications > The Beehive Ring and Multiring Lock Protocols