[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Experimenting with PlusCal / TLA+ at Dropbox

Hi all,

I work at Dropbox, and we recently had a "Hack Week" (i.e. a week to work on anything we want); I chose to spend the week experimenting with TLA+ / PlusCal for specifying components of our production systems.

Anyway, I just wanted to share the results of my week with this list.  I ended up using PlusCal to specify one of our protocols for maintaining strong consistency between a cache and the underlying database.  I've attached a recent version of the spec; here are a few additional remarks:
Overall, I thought this was a really interesting and worthwhile exercise.  I definitely plan to write a PlusCal or TLA+ spec next time I get the opportunity to design a complicated component involving lots of concurrency or subtle state transitions.  I also think I've managed to generate some interest among my coworkers; if I'm lucky, I'll be able to get some of them to add these great tools to their toolbox as well.

Thanks for reading; I'd love to hear from you if you have any questions or suggestions!


Attachment: ConsistentKV.pdf
Description: Adobe PDF document