-
InfluxDB
Power Real-Time Data Analytics at Scale. Get real-time insights from all types of time series data with InfluxDB. Ingest, query, and analyze billions of data points in real-time with unbounded cardinality.
I threw TLA+ at a few fine-grained locking algorithms I wrote. Here is one such model. The actual implementation is more complex than the model, in particular because the real implementation of this code handles multiple concurrent resource requests, but they are "independent" enough that I can probably just prove a model with just one resource; and, as Lamport said once, the model code doesn't have to be particuarly well optimized, whereas if you are breaking locks, you probably have substantially optimized already.
NOTE:
The number of mentions on this list indicates mentions on common posts plus user suggested alternatives.
Hence, a higher number means a more popular project.