Basho coworking office hours are every month. The meetup is during the day to come and hack on, deploy or just get a kick start on Riak, Riak CS or discuss NoSQL Solutions and Riak. Our first Coworking Office Hours will be from 9am until 11am on February the 4th. The regular meeting is scheduled for the same day at 7:00pm, generally we always meet at NedSpace unless otherwise mentioned in the meetup.

This Monday meet Eric Redmond AKA @coderoshi and I AKA @adron will be here to answer any questions, strike up discussions about Riak or help with any architectural or data oriented questions you may have. So come and join us, cheers!

Is the siloed internet over? It's too early to tell, but personal cloud is showing tremendous promise as a counter-paradigm that holds the promise of both providing most or all of the services that we currently enjoy and doing so in a way that is vastly more consistent with more stringent understanding of privacy and consent. While there are numerous countries making slow progress on the personal cloud front, none, as far as I know, are considering Riak as a data store for personal clouds. In this talk, I'd like to make the case for Riak as being an ideal technology for this.

Come on by the New Relic offices to talk Riak! Basho core engineer Jordan West will be discussing broader level distributed systems topics as well as what's going on with Riak --> 2.0!!!!

Pizza and beer too!

Title:

Formally Verifying Implementations of Distributed Systems

Abstract:

Distributed systems are difficult to implement correctly because they must handle both concurrency and failures: machines may crash at arbitrary points and networks may reorder, drop, or duplicate packets. Further, their behavior is often too complex to permit exhaustive testing. In this talk, we'll survey the Verdi project which provides a framework for implementing and formally verifying implementations of distributed systems in Coq. Verdi eases the verification burden by enabling developers to first verify their system under an idealized fault model, then transfer the resulting correctness guarantees to a more realistic fault model without any additional proof burden. Using this approach, the Verdi team produced the first correctness proof for an implementation of the Raft distributed consensus protocol.

Bio:

Zach Tatlock is an Assistant Professor in Computer Science and Engineering at the University of Washington where he leads the Programming Languages and Software Engineering (PLSE) group. He received his PhD from UC San Diego and BS from Purdue (where he took nearly every course with Bill Harris!). His research draws upon proof assistants, SMT solvers, and type systems to improve software reliability and security in domains ranging from distributed systems and compilers to web browsers. He can juggle and solve Rubik’s cubes, but not at the same time.