BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Memento EPFL//
BEGIN:VEVENT
SUMMARY:IC Colloquium: Optimizing the Automated Programming Stack
DTSTART:20190408T101500
DTEND:20190408T111500
DTSTAMP:20260407T065900Z
UID:c1486185c66773c7df7b0f24f72c147370ba153a0354f10858f2bb78
CATEGORIES:Conferences - Seminars
DESCRIPTION:By: James Borholt - University of Washington\nIC Faculty candi
 date\n\nAbstract:\nThe scale and pervasiveness of modern software poses a 
 challenge for programmers: software reliability is more important than eve
 r\, but the complexity of computer systems continues to grow. Automated pr
 ogramming tools are powerful weapons for programmers to tackle this challe
 nge: verifiers that check software correctness\, and synthesizers that gen
 erate new correct-by-construction programs. These tools are most effective
  when they apply domain-specific optimizations\, but doing so today requir
 es considerable formal methods expertise.\n \nIn this talk\, I present a 
 new application-driven approach to optimizing the automated programming st
 ack underpinning modern domain-specific tools. I will demonstrate the impo
 rtance of programming tools in the context of memory consistency models\, 
 which define the behavior of multiprocessor CPUs and whose subtleties ofte
 n elude even experts. Our new tool\, MemSynth\, automatically synthesizes 
 formal descriptions of memory consistency models from examples of CPU beha
 vior. We have used MemSynth to synthesize descriptions of the x86 and Powe
 rPC memory models\, each of which previously required person-years of effo
 rt to describe by hand\, and found several ambiguities and underspecificat
 ions in both architectures. I will then present symbolic profiling\, a new
  technique we designed and implemented to help people identify the scalabi
 lity bottlenecks in automated programming tools. These tools use symbolic 
 evaluation\, which evaluates all paths through a program\, and is an execu
 tion model that defies both human intuition and standard profiling techniq
 ues. Symbolic profiling diagnoses scalability bottlenecks using a novel pe
 rformance model for symbolic evaluation that accounts for all-paths execut
 ion. We have used symbolic profiling to find and fix performance issues in
  8 state-of-the-art automated tools\, improving their scalability by order
 s of magnitude\, and our techniques have been adopted in industry. Finally
 \, I will give a sense of the importance of future application-driven opti
 mizations to the automated programming stack\, with applications that insp
 ire improvements to the stack and in turn beget even more powerful automat
 ed tools.\n\nBio:\nJames Bornholt is a Ph.D. candidate in the Paul G. Alle
 n School of Computer Science & Engineering at the University of Washington
 \, advised by Emina Torlak\, Dan Grossman\, and Luis Ceze. His research in
 terests are in programming languages and formal methods\, with a focus on 
 automated program verification and synthesis. His work has received an ACM
  SIGPLAN Research Highlight\, two IEEE Micro Top Picks selections\, an OSD
 I best paper award\, and a Facebook Ph.D. fellowship.\n\nMore information
LOCATION:BC 420 https://plan.epfl.ch/?room==BC%20420
STATUS:CONFIRMED
END:VEVENT
END:VCALENDAR