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.