On technology transfer - Formal Methods and Tools

Sep 17, 2015 - Android (3.0+) ... Android (5. ..... demonstrated at the outset, any company founded to .... use – a no-go even for an evaluation by a company.
1MB Sizes 4 Downloads 148 Views
On technology transfer: experience from the CARP project... and beyond Anton Lokhmotov, dividiti Lorentz Center workshop on verification of concurrent and distributed software, Leiden, 17 September 2015

A view from @LegoAcademics

“The @LegoAcademics wonder how much time Newton spent courting strategic industry commercialization partners.”

My view: courting industry is good! “The @LegoAcademics wonder how much time Newton spent courting strategic industry commercialization partners.” ● ● ● ●

Must be a frustrated response to research funding guidelines. Indeed, not all kinds of research can be commercialised. But as this talk should hopefully demonstrate, those kinds than can would do well from collaborating with industry. (After all, even Newton, according to a popular account, had a contact with… )

My background ● ● ●

PhD (Cambridge, 2008); MSc (Moscow PhysTech, 2004). (2008-2009) Post-doctoral research associate at Imperial College London. (2010-2015) Technical lead and manager for the GPU compute compilers for the ARM Mali GPU series: ○ Industry-first OpenCL 1.1 Full Profile implementation for mobile. ○ Industry-first RenderScript GPU support. ○ Innovation and technology transfer champion: ■ GPUVerify integrated into Mali Graphics Debugger (in this talk). ■ PENCIL, a platform-neutral compute intermediate language. ■ PENCIL-to-OpenCL polyhedral compiler. ■ BLAS for Mali, an autotuned VOBLA-to-PENCIL implementation. ■ Collective Knowledge validated for performance analysis and predictive analytics (flagship activity of dividiti).

Alastair F. Donaldson ● ● ● ●



Advisor in Software Reliability, dividiti (since 2015). Senior Lecturer / Leader of the Multicore Programming Group (http: //multicore.doc.ic.ac.uk), Imperial College London (since 2011). Coordinator, EU CARP project (http://carpproject.eu, 2011-2015). ○ Involving ARM, INRIA, Codeplay, Monoidics (acquired by Facebook). GPUVerify (with Multicore Programming Group + Shaz Qadeer, Microsoft) ○ Static analysis tool for GPU kernels (OOPSLA’12, OOPSLA’13, POPL’ 14, CAV’14). ○ Integrated with the ARM Mali Graphics Debugger (since v2.1). CLsmith (with Christopher Lidbury, Andrei Lascu and Nathan Chong) ○ Random test generator for OpenCL compilers (PLDI’15). ○ Found 50+ compiler bugs in OpenCL drivers from Intel, AMD, NVIDIA, Altera, ARM.

Specialisation is key to efficiency High performance systems support innovative applications ●

Energy efficiency has become as important as execution speed.

Heterogeneous hardware ● ●

Clusters of general-purpose processors (e.g. ARM big.LITTLE CPUs). Special-purpose accelerators (e.g. ARM Mali GPUs).

Software? ●

(this talk)

Compute APIs: 2007-2014 API

CUDA

OpenCL

DirectCompute

RenderScript

Originator

NVIDIA

Khronos (Apple)

Microsoft

Google

Year

2007

2008

2009

2011

Area

HPC, desktop

HPC, desktop, mobile, embedded

Desktop

Mobile

OS

Windows, Linux, MacOS

Windows, Linux, MacOS (10.6+)

Windows (Vista+)

Android (3.0+)

Devices

GPUs (NVIDIA)

CPUs, GPUs, etc.

GPUs (desktop)

CPUs, GPUs

Work unit

Kernel

Kernel

Compute shader

Compute script

Language

CUDA C/C++

OpenCL C

HLSL

Script C

Form

Source, PTX

Source, SPIR

Source, bytecode

LLVM bitcode

Compute APIs: 2014-? API

CUDA, OpenCL, DirectCompute, C++ AMP...

Metal

Vulkan

Appl