The Mailbox Problem

This paper addresses a little synchronization problem that I first thought about in the 1980s. When Gafni visited MSR Silicon valley in 2008, I proposed it to him and we began working on it. I thought the problem was unsolvable, but we began to suspect that there was a solution. Gafni had an idea for an algorithm, but instead of trying to understand the idea, I asked for an actual algorithm. We then went through a series of iterations in which Gafni would propose an algorithm, I’d code it in PlusCal (see [161]) and let the model checker find an error trace, which I would then give to him. (At some point, he learned enough PlusCal to do the coding himself, but he never installed the TLA+ tools and I continued to run the model checker.) This process stopped when Aguilera joined MSR and began collaborating with us. He turned Gafni’s idea into an algorithm that the model checker approved of. Gafni and Aguilera came up with the impossibility results. Aguilera and I did most of the actual writing, which included working out the details of the proofs.We propose and solve a synchronization problem called the mailbox problem, motivated by the interaction between devices and processor in a computer. In this problem, a postman delivers letters to the mailbox of a housewife and uses a flag to signal a non-empty mailbox. The wife must remove all letters delivered to the mailbox and should not walk to the mailbox if it is empty. We present algorithms and an impossibility result for this problem.