Seminar by John Launchbury

Thanks to NICTA, John Launchbury will be in Sydney next week. He contributed in many ways to the development of the Haskell programming language and provided practical proof of the benefits of functional programming and formal methods by founding and leading the company Galois, Inc.

On Friday (20 January), John will give a presentation at the School of Computer Science and Engineering (CSE) of the University of New South Wales. The details are as follows.

 

Time: 20 January 2012 (Friday), 10.30AM

Location: CSE Seminar room (K17_113), Level 1, CSE Building (K17)

 

Title: A Snapshot on Secure Computation

Speaker: John Launchbury (Galois, Inc.)

Abstract

There is growing interest in performing computation on encrypted data, partly motivated by the challenges of cloud computing. As we lose control of the location of our data, we still want to retain control of the confidentiality and/or integrity of our data. If we could encrypt our data (either for confidentiality, or for integrity) and then have the cloud operators perform computations on the data in the encrypted form, then we may have the best of both worlds: the cloud supplies storage and computational resources, while the encryption provides guarantees about what happens to the data.

Recent theoretical breakthroughs in homormorphic encryption have raised the possibility of this working in practice, though there are very many challenging practical considerations to overcome first. In the meantime, a simpler method of secure shared computation is approaching practicality---the main limiting factor is the network communication required. The main weakness of sharing schemes is that they rely on the fairly weak security model of "honest but curious", though there are newer techniques to weaken this assumption.

In this talk we describe the current state of the art, and provide some specific insights into how to build plausibly efficient algorithms for shared computation.

Bio

Dr. John Launchbury is Chief Scientist of Galois, Inc. John founded Galois in 1999 to address challenges in Information Assurance through the application of Functional Programming and Formal Methods. Under his leadership, formerly as CEO, the company has grown strongly, successfully winning and delivering on multiple contracts for more than a decade. Prior to founding Galois, John was a full professor in Computer Science and Engineering at the Oregon Graduate Institute School of Science and Engineering at OHSU. John received First Class Honors in Mathematics from Oxford University in 1985. He holds a Ph.D. in Computing Science from University of Glasgow and won the British Computer Society's distinguished dissertation prize. In 2010, John was inducted as a Fellow of the Association for Computing Machinery (ACM) for his contributions to functional programming.

 

Seminar by John Hughes & Simon Peyton Jones @ UNSW

As part of YOW! 2011 (the Australian Software Developer Conference), Simon Peyton Jones and John Hughes will be in Sydney on the 7th and 8th of December 2011. On the evening of the 7th, they will appear at the YOW! Night Sydney.

On Thursday (8 December), John and Simon will give two presentations at the School of Computer Science and Engineering (CSE) of the University of New South Wales. The details are as follows.

Time: 8 December 2011, 10AM

Location: CSE Seminar room (K17_113), Level 1, CSE Building (K17)

 

 

Talk #1

Title: Accelerating race condition detection through procrastination

Speaker: John Hughes (Chalmers University & Quviq AB)

Abstract

Race conditions are notoriously frustrating to find, and good tools can help. The main difficulty is reliably provoking the race condition. In previous work we presented a randomising scheduler for Erlang that helps with this task.

In a language without pervasive shared mutable state, such as Erlang, performing scheduling decisions at random uncovers race conditions surprisingly well. However, it is not always enough. We describe a technique, procrastination, that aims to provoke race conditions more often than by random scheduling alone. It works by running the program and looking for pairs of events that might interfere, such as two message sends to the same process. Having found such a pair of events, we re-run the program but try to provoke a race condition by reversing the order of the two events.

We apply our technique to a piece of industrial Erlang code. Compared to random scheduling alone, procrastination allows us to find minimal failing test cases more reliably and more quickly.

John Hughes

John Hughes has worked with functional programming since 1980, was one of the designers of Haskell, and has been heavily involved with Erlang in recent years. In 2000 he and Koen Claessen published the first version of QuickCheck, a software testing tool which recently won the ACM SIGPLAN award for Most Influential Paper from ICFP in that year. He has focussed more and more on testing since then, co-founding Quviq AB in 2006 to market a commercial version of QuickCheck. He is currently both a Professor at Chalmers University, Sweden, and CEO of Quviq AB.

 

Talk #2

Title: Termination Combinators Forever

Speaker: Simon Peyton Jones (Microsoft Research)

Abstract

Nobody wants their compiler, or theorem prover, to go into an infinite loop, but making sure that never happens usually means applying some over-conservative heuristic like “never unfold a recursive function”. Approaches like that don’t work at all when you are doing partial evaluation or supercompilation, which fundamentally depend on inlining recursive functions. 

What we need is an online termination test. That is easier said than done; it is easy to make a mistake. In this talk I’ll describe a new combinator library that lets you build complex termination tests by combining simpler ones, while guaranteeing that that the result really is a termination test. The library elegantly encapsulates some clever mathematical ideas on well-quasi orders the cunning details are hidden from the customer.

I’ll use Haskell as the language of exposition, but you don’t need to be a Haskell guru to understand it, and the library would work equally well in other languages.

Simon Peyton Jones

Simon Peyton Jones, MA, MBCS, CEng, graduated from Trinity College Cambridge in 1980. After two years in industry, he spent seven years as a lecturer at University College London, and nine years as a professor at Glasgow University, before moving to Microsoft Research (Cambridge) in 1998.

His main research interest is in functional programming languages, their implementation, and their application. He has led a succession of research projects focused around the design and implementation of production-quality functional-language systems for both uniprocessors and parallel machines. He was a key contributor to the design of the now-standard functional language Haskell, and is the lead designer of the widely-used Glasgow Haskell Compiler (GHC). He has written two textbooks about the implementation of functional languages.

More generally, he is interested in language design, rich type systems, software component architectures, compiler technology, code generation, runtime systems, virtual machines, and garbage collection. He is particularly motivated by direct use of principled theory to practical language design and implementation — that's one reason he loves functional programming so much.

 

Data Parallel Haskell and Repa for GHC 7.2.1

As an add-on to the just released GHC 7.2.1, Ben just uploaded the Data Parallel Haskell packages (version 0.5) to Hackage. This version is still largely a technology preview and not a production-ready system. Nevertheless, it is significantly more robust than previous versions, especially for programs with a statically fixed depth of nesting of parallelism. For further information on how to install and use Data Parallel Haskell (DPH), see the DPH documentation.

Ben simultaneously released the companion library Repa (version 2.1.1.6) for use with GHC 7.2.1. In contrast to the DPH libraries, which enable nested data parallelism, Repa implements parallel, shape-polymorphic, regular multi-dimensional arrays.  See this previous post for some more details.

Real-time edge detection with the latest release of the parallel array library Repa

We just released version 2.0.0.1 of the Repa array library for Haskell, which includes Ben's recent work on high-performance, parallel stencil computations. The work on stencil computations is described in detail in a draft paper entitled 
Efficient Parallel Stencil Convolution in Haskell. Be sure to check out Ben's screencast of a real-time edge detection application, written in Objective-C and Haskell, using the new Repa library. For more details, see Ben's blog post.

Simon Peyton Jones: parallel = functional

Simon Peyton Jones recently gave a talk on parallel programming in Haskell at Functional Programming eXchange 2011. It provides a comprehensive overview of the state of the art of parallel programming in Haskell. It covers Software Transactional Memory, Erlang-style communicating processes, parallel strategies as well as our Data Parallel Haskell, Repa, and Accelerate projects. Watch the video.

Status Update on the LLVM Backend for GHC

GHC's new LLVM backend, developed by David Terei as part of his Honours thesis at PLS, is being made ready for inclusion into the main GHC repository.  The backend requires a new calling convention to be added to LLVM.  David got a patch including the new calling convention accepted into the main LLVM distribution, just in time to become part of the forthcoming LLVM 2.7 release — the inclusion into 2.7 has been confirmed.

The next step is to incorporate a number of suggestions by Simon Marlow on how to improve the LLVM backend code.  After that, the patch should be ready to go into the tree!

David will be on an internship at GHC HQ at Microsoft Research Cambridge in the second quarter of this year, specifically to work on the GHC LLVM backend.