Search

Log analysis is required in many domains, and especially in the emerging field of cloud computing. Cloud applications are often built by composing diverse services. When something goes wrong, finding the root cause of the problem can be difficult. Many services are only reachable through their Application Programming Interfaces (APIs) with no possibility for live introspection. In this context, logs become an essential tool for monitoring and debugging. Cloud services typically generate very large quantities of log messages, with formats that may not be well specified and may vary over time. In this paper, we present CloudLens, a language for the analysis of semi-structured textual data as found in logs, and specify its formal semantics. CloudLens is a reactive language and views logs as streams of objects. Our objective is to facilitate exploring the contents of logs interactively and to write reusable analyses succinctly, using familiar constructs. We implemented an interpreter for the Apache Zeppelin notebook to provide an interactive IDE. Our prototype implementation is open source and we report on a detailed case study using logs from the Apache OpenWhisk project.

Companies want to offer chat bots to their customers and employees which can answer questions, enable self-service, and showcase their products and services. Implementing and maintaining chat bots by hand costs time and money. Companies typically have web APIs for their services, which are often documented with an API specification. This paper presents a compiler that takes a web API specification written in Swagger and automatically generates a chat bot that helps the user make API calls. The generated bot is self-documenting, using descriptions from the API specification to answer help requests. Unfortunately, Swagger specifications are not always good enough to generate high-quality chat bots. This paper addresses this problem via a novel in-dialogue curation approach: the power user can improve the generated chat bot by interacting with it. The result is then saved back as an API specification. This paper reports on the design and implementation of the chat bot compiler, the in-dialogue curation, and working case studies.

Since our work on verification sixteen years ago, our views of the role of verification, and the centrality of correctness, have evolved. In our presentation, we’ll talk about some of our concerns about the limitations of this kind of technology, including: usability as a key factor; the unknowable properties of the environment; and the inadequacy of specifications as a means of capturing users’ desires. We’ll describe two approaches we’re currently working on to mitigate these concerns — (1) moving to higher level abstractions with correctness by construction and (2) focusing on the conceptual structure of applications — and will argue that, combined with traditional verification tools, these offer the possibility of applications that are both usable and correct.

Continuous data streams are ubiquitous and represent such a high volume of data that they cannot be stored to disk, yet it is often crucial for them to be analyzed in real-time. Stream processing is a programming paradigm that processes these immediately, and enables continuous analytics. Our objective is to make it easier for analysts, with little programming experience, to develop continuous analytics applications directly. We propose enhancing a spreadsheet, a pervasive tool, to obtain a programming platform for stream processing. We present the design and implementation of an enhanced spreadsheet that enables visualizing live streams, live programming to compute new streams, and exporting computations to be run on a server where they can be shared with other users, and persisted beyond the life of the spreadsheet. We formalize our core language, and present case studies that cover a range of stream processing applications.

Model checking is a proven successful technology for verifying hardware. It works, however, on only finite state machines, and most software systems have infinitely many states. Our approach to applying model checking to software hinges on identifying appropriate abstractions that exploit the nature of both the system, S, and the property, θ, to be verified. We check θ on an abstracted, but finite, model of S. Following this approach we verified three cache coherence protocols used in distributed file systems. These protocols have to satisfy this property: “If a client believes that a cached file is valid then the authorized server believes that the client's copy is valid.” In our finite model of the system, we need only represent the “beliefs” that a client and a server have about a cached file; we can abstract from the caches, the files' contents, and even the files themselves. Moreover, by successive application of the generalization rule from predicate logic, we need only consider a model with at most two clients, one server, and one file. We used McMillan's SMV model checker; on our most complicated protocol, SMV took less than 1 s to check over 43600 reachable states.

Model checking is a proven successful technology for verifying hardware. It works, however, on only fInite state machines, and most software systems have infInitely many states. Our approach to applying model checking to software hinges on identifying appropriate abstractions that exploit the nature of both the system, S, and the property, phi to be verifIed. We check phi on an abstracted, but fInite, model of S. Following this approach we verified three cache coherence protocols used in distributed file systems. These protocols have to satisfy this property: 'If a client believes that a cached file is valid then the authorized server believes that the client's copy is valid.' In our finite model of the system, we need only represent the 'beliefs' that a client and a server have about a cached file; we can abstract from the caches, the files' contents, and even the files themselves. Moreover, by successive application of the generalization rule from predicate logic, we need only consider a model with at most two clients, one server, and one file. We used McMillan's SMV model checker; on our most complicated protocol, SMV took less than 1 second to check over 43,600 reachable states.