tag:blogger.com,1999:blog-8436330762136344379.post6849910645114883630..comments2024-03-18T20:09:27.497-04:00Comments on Metadata: TLA+ specification of the bounded staleness and strong consistency guaranteesMurathttp://www.blogger.com/profile/07842046940394980130noreply@blogger.comBlogger2125tag:blogger.com,1999:blog-8436330762136344379.post-16531849139642697412018-08-31T19:04:13.277-04:002018-08-31T19:04:13.277-04:00Replying to myself: there is only one process doin...Replying to myself: there is only one process doing multicast so it doesn't matter. :)<br /><br />PS: I didn't see a definition for send?Anonymousnoreply@blogger.comtag:blogger.com,1999:blog-8436330762136344379.post-37578808047201388312018-08-31T18:51:48.587-04:002018-08-31T18:51:48.587-04:00Hi,
Thank you for posting about TLA+, you're ...Hi,<br /><br />Thank you for posting about TLA+, you're one of several people who contributed to educate me on this powerful tool, which I now use in my day job. :)<br /><br />A question: in your spec, the multicast macro atomically appends a message to all chans: all processes receive messages in the same order (that isn't the case in a less sophisticated network). To me this would mean that you (implicitly?) rely on some atomic broadcast system (like Virtual Synchrony). Is that on purpose? Does it matter?Anonymousnoreply@blogger.com