Skip to content

Seattle Scalability - Verification of Distributed Algorithms with TLA+ +CTO Tune

Photo of clive boulton
Hosted By
clive b. and Bradford S.
Seattle Scalability - Verification of Distributed Algorithms with TLA+ +CTO Tune

Details

Verification of Distributed Algorithms with TLA+

w/ Alena Hall (@Lenadroid (https://twitter.com/lenadroid))

Verification of distributed algorithms comes is useful, because testing doesn’t usually work really well for concurrent and distributed systems. We can check the correctness of simple steps and chains of steps by testing, we might even find some implementation bugs, but it’s more complex to reproduce a non trivial error.

If we had a way to verify the algorithm we want to implement and prove that it is correct, we could avoid some tricky and hard to solve errors.

TLA+ can help us with that. TLA+ is a formal specification language developed by Leslie Lamport. It is used to design, model, document, and verify concurrent systems.

We will go through use cases, reasons, and an example of a TLA+ spec for a distributed algorithm.

Amazon Athena -- and the Wild World of Distribute SQL Query Engines

w/ Dan Koch, CTO of Tune

"We're coming up on the tenth anniversary of when the first bytes of Apache Hive were put together, and the concept of applying SQL queries to distributed data warehouses has covered a profound amount of ground since then. We'll talk about the most recent developments in this space -- including what Amazon Athena provides for AWS users and how to use it most effectively."

This meetup focuses on Scalability and technologies to enable handling large amounts of data: Hadoop, HBase, distributed NoSQL databases, and more!

There's not only a focus on technology, but also everything surrounding it including operations, management, business use cases, and more.

We've had great success in the past, and are growing quickly! Previous guests were from Twitter, LinkedIn, Amazon, Cloudant, Microsoft, 10gen/MongoDB, and more.

This month's guests:

(more)

Our format is flexible: We usually have 2 speakers who talk for ~30 minutes each and then do Q+A plus discussion (about 45 minutes each talk) finish by 8:45.

There'll be bites, beer and wine c/o Tune!

Meetup Location:

https://secure.meetupstatic.com/photos/event/2/e/5/8/600_460031864.jpeg

90 Blanchard St (enter via basement walkway). It's the old Belltown Billiards space.

For parking, we suggest street parking or there are a couple lots around the building.

Thanks to our friends at TUNE for their support and making the space, food, and beverages for this upcoming event possible.

Doors open 30 minutes ahead of show-time. Please show up at least 15 minutes early out of respect for our first speaker.

Photo of Seattle Scalability Meetup group
Seattle Scalability Meetup
See more events
Tune
90 Blanchard St. · Seattle, WA