At its most basic, TLA+ is a written description of what a system is supposed to do. More specifically, TLA+ is a specification language for formally defining the behavioural properties of a system. TLA+ is based on temporal logic, which is built on top of first-order logic and set theory, and provides some conveniences for working with large specifications for complex systems. You can think of a TLA+ specification as mostly ordinary math and logic, glued together with temporal logic for parts requiring it. ...

I’ve been helping define some concurrent algorithms and I’m struggling with a number of issues: concurrent algorithms are difficult to design, they are often difficult to implement, and, even after they are designed, are difficult to guarantee that they are correct. This lead me into some research on formal specifications for algorithms, and how they can help. Finally, I settled on TLA+ as a viable tool for just such a problem. ...

Title and Author of Paper WebTables: Exploring the Power of Tables on the Web. M.J. Cafarella et al. Summary WebTables is a project to extract and process HTML tables from Google’s serach index. It attempts to answer two questions: what are some effective techniques for searching structured data at search engine scale, and what can be derived from analyzing a large corpus of HTML tables? Web documents often contain structured and relational data embedded in HTML tables. The WebTables project extracted 14.1 billion English language HTML tables and further filtered those down to 154 million tables that contain structured data. From this data, we have the potential to determine semantic information embedded in the web, create visualizations, and integrate web documents into new applications. ...

Title and Author of Paper Combining Systems and Databases: A Search Engine Retrospective. Eric A. Brewer. Summary Search engines manage data and respond to queries, which provides some similarities to databases. However, search engines are really an application-specific system built to handle large datasets. This system can leverage databases, or not, depending on the system goals. This paper describes a search engine design that leverages the ideas and vocabulary of the database community. ...

Amazon’s Simple Queue Service (SQS) provides durable messaging guarantees and is an excellent backbone for messaging services. However, SQS does not support “fan-out” of messages so that multiple consuming services can each receive a copy of a message. This means that true publish-subscribe messaging requires some additional work. This post describes some architectural choices that provide durable publish-subscribe messaging using SQS by tracking messaging subscribers using a database, and matching published messages to interested subscribers. ...

Title and Author of Paper The Anatomy of a Large-Scale Hypertextual Web Search Engine. Sergey Brin and Lawrence Page. Summary This paper describes the underpinnings of the Google search engine. The paper presents the initial Google prototype and describes the challenges in scaling search engine technology to handle large datasets. At the time of writing, the main goal of Google is to improve the quality of web searches by taking advantage of the existing link data embedded in web pages to calculate the quality of a page. ...

Title and Author of Paper Consistency Analysis in Bloom: a CALM and Collected Approach. Alvaro et al. Summary Distributed programming is difficult for even experienced developers to get correct. Understanding the tradeoff between consistency, availability, and latency, while guaranteeing data correctness, provides a wealth of problems for the application developer. This paper presents a language and method for programmatically verifying distributed consistency. CALM - Consistency and Logical Monotonicity There is a connection between distributed consistency algorithms and logical monotonicity, that is, our programs must be correct even in the face of the delay and re-ordering of messages and data across different nodes in a system. By designing programs with order independence, we can ensure that the logic of the system is maintained within a distributed environment. ...

When designing Workiva’s durable messaging system we took a hard look at using Amazon’s Kinesis as the message storage and delivery mechanism. At first glance, Kinesis has a feature set that looks like it can solve any problem: it can store terabytes of data, it can replay old messages, and it can support multiple message consumers. But if you dig a little deeper you will find that Kinesis is well suited for a very particular use case, and if your application doesn’t fit this use case, Kinesis may be a lot more trouble than it’s worth. ...

Architecture is the bridge between (often abstract) business goals and the final (concrete) resulting system. – Software Architecture in Practice A software architect should act as a bridge between business stakeholders and technical stakeholders. To be this bridge requires understanding the business problem being solved, and being able to distill that problem into a technical solution that a software team can implement. In essence, the architect acts as a technical business analyst that helps to define the needs of an organization and recommend solutions that deliver value to stakeholders. It just so happens that an architect’s stakeholders include project managers, software developers, management, and other software architects. This article describes how a software architect can apply methods from business analysis to make their job easier and to satisfy these different stakeholders. ...

Title and Author of Paper The CQL continuous query language: semantic foundations and query execution. Arasu et al. Summary CQL is a derivation of the SQL query language developed for running continuous queries over streams of data. The goals of the system are to provide a precise set of language semantics for running such continuous stream workloads. The paper starts by defining precise abstract semantics for continuous queries that cover two data types — streams and relations — and three classes of operators: ones that produce a relation from a stream, one that produces a relation from other relations, and one that produces a stream from a relation. These semantics are defined independent of the underlying implementation. The second portion of this paper defines how CQL instantiates these abstract semantics using existing SQL specifications and some new CQL additions. ...