Oradores Convidados

Flávio Junqueira

Flávio Junqueira is a research scientist with Yahoo! Research in Barcelona. He holds a PhD degree from University of California San Diego in computer science, a MSc degree in Electrical Engineering from COPPE/UFRJ in Rio de Janeiro, and a BS degree cum laude in Electrical Engineering from UFRJ in Rio de Janeiro. His research work has been concentrated on distributed systems and algorithms, and he has worked on projects related to the modeling of failures and vulnerabilities in distributed systems, to the design of distributed algorithms, and to information retrieval in large-scale distributed systems. He is the recipient of a number of awards and nominations, such as the CSE Department best PhD dissertation award, a nomination to the ACM PhD Dissertation award, and the best paper awards at ACM CIKM 2009 and USENIX ATC 2010. He is an active contributor to open source projects, such as Hadoop and ZooKeeper from the Apache Software Foundation.

Keynote: Distributed Coordination

Abstract: Distributed coordination is critical for Web-scale distributed systems. Examples of such systems are distributed file systems used for data processing (e.g., GFS, HDFS1), scalable data storage systems (e.g., BigTable), and Web search infrastructure (e.g., Crawlers, Indexers). Coordination in these systems can take the form of configuration metadata or more sophisticated synchronization primitives such as locks and leader election. Some of these coordination needs arise frequently enough to justify the design and implementation of systems for coordination.

In this presentation, we motivate the design of systems to enable the co- ordination of distributed applications, and discuss the design of two systems currently used in production: Chubby and ZooKeeper. Chubby is a lock service that exposes a file-system-like interface, including operations to acquire and release locks. Chubby is a replicated service and has the master of a replica group initiating all operations to guarantee that they are linearizable. Chubby also enables clients to cache the data of frequently accessed files and manages such caches directly, invalidating cached content explicitly upon updates. ZooKeeper also exposes a file-system-like interface and is a replicated service, but makes different design choices. ZooKeeper is not a lock service and it does not guarantee that all operations are linearizable. Instead it guarantees FIFO order for the operations of individual clients and linearizability of update operations (operations that change the state of ZooKeeper). A weaker consistency guarantee, however, does not imply a reduction of expressiveness when it comes to implementing synchronization primitives. As for client-side caches, ZooKeeper does not manage them directly, and instead uses watches to notify clients of changes.

We finally present ZooKeeper evaluation results and discuss our experience to date with ZooKeeper in production. Our evaluation results show that we can obtain thousands of operations per second with read-dominant workloads, which meets the requirements of current applications.

José Nuno Oliveira

José Nuno Oliveira (http://www.di.uminho.pt/~jno) is currently Associate Professor of Computer Science. He graduated from the U.Porto and received his MSc and PhD in Computer Science from the U.Manchester, where he became interested in formal methods and transformational techniques. He is a member of the Formal Methods Europe (FME) association, where he convenes a subgroup on education, and of the scientific committee of the MAP-i doctoral programme. He is also a member of the IFIP WG2.1 - Algorithmic Languages and Calculi. Since his PhD work on data-flow program transformation, he became interested in program calculi and transformational design. He has served the programme committee of several conferences in the series of FME symposia, MPC, TFM, SEFM, SBMF, ICTAC, ESOP, etc. He was co-chair of MPC'00, FME'00 and TFM'09.

Keynote:Hands on a verification challenge: proving a journaled file system correct

Abstract: In the context of the Verifiable File System (VFS) challenge put forward by Rajeev Joshi and Gerard Holzmann, this talk will address the refinement of an abstract file store model into a journaled (flash) data model catering for wear leveling and recovery from power loss. Such refinement steps are carried out within a simple verification life-cycle where model checking in Alloy goes hand in hand with manual proofs carried out in the (pointfree) algebra of binary relations. This provides ample evidence of the positive impact of Alloy’s lemma “everything is a relation” on software verification, in particular in its entailing induction-free proofs about data structures such as stores and lists. (Joint work with Miguel Ferreira, SIG, Amsterdam).

Barrett Bryant (Sessão CoRTA)

Barrett R. Bryant is Professor and Associate Chair of Computer and Information Sciences at the University of Alabama at Birmingham (UAB). He received his B. S. in computer science from the University of Arkansas at Little Rock in 1979 and his Ph. D. in computer science from Northwestern University in 1983, after which he joined UAB. He has held visiting appointments at a number of institutions, including Ibaraki University, Hitachi, Japan, the Naval Postgraduate School, Monterey, California, USA, and Tsinghua University, Beijing, China. His research interests include theory and implementation of programming languages, formal specification of software systems, and component-based software engineering, and he has authored or co-authored over 120 published papers in these areas. He serves on the Steering Committee of EDOC (Enterprise Computing conference) and SAC (ACM Symposium on Applied Computing), and was formerly Chair of the ACM Special Interest Group on Applied Computing (2003-2009). He is a member of EAPLS, and a senior member of ACM and IEEE. Further details are available at http://www.cis.uab.edu/bryant.

Keynote: Grammar Inference Technology Applications in Software Engineering

Abstract: There are many problems whose solutions take the form of patterns that may be expressed using grammars (e.g., speech recognition, text processing, genetic sequencing, programming language development, etc.). Construction of these grammars is usually carried out by computer scientists working with domain experts. Grammar inference (GI) is the process of learning a grammar from examples, either positive (i.e., the pattern should be recognized by the grammar) and/or negative (i.e., the pattern should not be recognized by the grammar).

This talk will present the application of grammar inference to software engineering, including recovery of domain-specific language (DSL) specifications from example DSL programs and recovery of a meta model from instance models which have evolved independently of the original meta model.

Further details are available at http://www.cis.uab.edu/softcom/GrammarInference.