arXiv.itsnick.co

an independent field guide to 23 million papers from arXiv & OpenAlex — not affiliated with arXiv.org

Author

Adam Procter

25 papers · 2008–2019

2008: 12009: 32010: 12011: 12012: 42013: 42014: 12015: 22016: 32017: 32018: 12019: 1
2008peak 4 in 20122019

Frequent co-authors

Papers

showing 1–25 of 25 RSS

Intel nGraph: An Intermediate Representation, Compiler, and Executor for Deep Learning

Scott Cyphers, Arjun K. Bansal, Anahita Bhiwandiwalla +18 more

cs.DC · · cited 149× · arXiv ↗ · more like this ·

The Deep Learning (DL) community sees many novel topologies published each year. Achieving high performance on each new topology remains challenging, as each requires some level of manual effort. This issue is compounded by the proliferation of frameworks and hardware platforms. The current approach, which we call "direct optimization", requires deep changes within each framework to improve the training performance for each hardware backend (CPUs, GPUs, FPGAs, ASICs) and requires $\mathcal{O}(fp)$ effort; where $f$ is the number of frameworks and $p$ is the number of platforms. While optimized kernels for deep-learning primitives are provided via libraries like Intel Math Kernel Library for Deep Neural Networks (MKL-DNN), there are several compiler-inspired ways in which performance can be further optimized. Building on our experience creating neon (a fast deep learning library on…

A virtual memory based runtime to support multi-tenancy in clusters with GPUs

Michela Becchi, Kittisak Sajjapongse, Ian Graves +3 more

Computer Networks and Communications · · cited 65× · DOI ↗ · more like this ·

Graphics Processing Units (GPUs) are increasingly becoming part of HPC clusters. Nevertheless, cloud computing services and resource management frameworks targeting heterogeneous clusters including GPUs are still in their infancy. Further, GPU software stacks (e.g., CUDA driver and runtime) currently provide very limited support to concurrency.

Semantics Driven Hardware Design, Implementation, and Verification with ReWire

Adam Procter, William L. Harrison, Ian Graves +2 more

Artificial Intelligence · · cited 20× · DOI ↗ · more like this ·

There is no such thing as high assurance without high assurance hardware. High assurance hardware is essential, because any and all high assurance systems ultimately depend on hardware that conforms to, and does not undermine, critical system properties and invariants. And yet, high assurance hardware development is stymied by the conceptual gap between formal methods and hardware description languages used by engineers. This paper presents ReWire, a functional programming language providing a suitable foundation for formal verification of hardware designs, and a compiler for that language that translates high-level, semantics-driven designs directly into working hardware. ReWire's design and implementation are presented, along with a case study in the design of a secure multicore processor, demonstrating both ReWire's expressiveness as a programming language and its power as a…

A Principled Approach to Secure Multi-core Processor Design with ReWire

Adam Procter, William L. Harrison, Ian Graves +2 more

Artificial Intelligence · ACM Transactions on Embedded Computing Systems · · cited 11× · DOI ↗ · more like this ·

There is no such thing as high assurance without high assurance hardware. High assurance hardware is essential because any and all high assurance systems ultimately depend on hardware that conforms to, and does not undermine, critical system properties and invariants. And yet, high assurance hardware development is stymied by the conceptual gap between formal methods and hardware description languages used by engineers. This article advocates a semantics-directed approach to bridge this conceptual gap. We present a case study in the design of secure processors, which are formally derived via principled techniques grounded in functional programming and equational reasoning. The case study comprises the development of secure single- and dual-core variants of a single processor, both based on a common semantic specification of the ISA. We demonstrate via formal equational reasoning that…

Model-driven design & synthesis of the SHA-256 cryptographic hash function in ReWire

William L. Harrison, Adam Procter, Gerard Allwein

Artificial Intelligence · · cited 7× · DOI ↗ · more like this ·

There are many algorithms whose implementations can benefit both from hardware acceleration and formal verification and we would like to develop high assurance implementations as rapidly as possible. Critical computing infrastructure like cryptographic algorithms are prime candidates both for such acceleration and for formal verification. We show how to derive a verifiable, hardware-accelerated implementation of the SHA-256 cryptographic hash in the ReWire functional hardware description language in which the hardware-software partitioning of the implementation is reflected in the type system itself.

Semantics-driven design and implementation of high-assurance hardware

Adam Procter

Artificial Intelligence · MOspace Institutional Repository (University of Missouri) · · cited 7× · OpenAlex ↗ · more like this ·

Modularity, that is the division of complex systems into less complex and more easily understood parts, is a pervasive concern in computer science, and hardware design is no exception.Existing hardware design languages such as Verilog and VHDL support modular design by enabling hardware designers to decompose designs into structural features that may be developed independently and connected together to form more complex devices.In the realm of high assurance for security, however, this sort of modularity is often of limited utility.Security properties are notoriously non-compositional, i.e. subsystems that independently satisfy some security property cannot necessary be relied upon to maintain that property when operating in tandem.The aim of this research is to establish semantically modular techniques for hardware design and implementation, in contrast to the conventional structural…

A programming model for reconfigurable computing based in functional concurrency

William L. Harrison, Ian Graves, Adam Procter +2 more

Hardware and Architecture · · cited 6× · DOI ↗ · more like this ·

FPGA programmability remains a concern with respect to the broad adoption of the technology. One reason for this is simple: FPGA applications are frequently implementations of concurrent algorithms that could be most directly rendered in concurrent languages, but there is little or no first-class support for concurrent applications in conventional hardware description languages. It stands to reason that FPGA programmability would be enhanced in a hardware description language with first-class concurrency. The starting point for this paper is a functional hardware description language with built-in support for concurrency called ReWire. Because it is a concurrent functional language, ReWire supports the elegant expression of common concurrency paradigms; we illustrate this with several case studies.

Provably Correct Development of reconfigurable hardware designs via equational reasoning

Ian Graves, Adam Procter, William L. Harrison +1 more

Hardware and Architecture · · cited 6× · DOI ↗ · more like this ·

There is a semantic gap between the hardware definition languages used to design and implement hardware and the languages and logics used to formally specify and verify them. Bridging this gap-i.e., constructing formal models from existing hardware artifacts-can be costly, time-consuming, and error prone-and yet utterly necessary if formal verification is to proceed. This work demonstrates that this gap can be collapsed by starting in a pure functional language that is also a hardware description language, and that equational style verifications may be performed directly on the source text of a hardware design, thereby significantly lowering the verification cost for reconfigurable designs. When combined with an efficient compiler, this methodology achieves both good performance and low cost verification.

Semantics-directed machine architecture in ReWire

Adam Procter, William L. Harrison, Ian Graves +2 more

Artificial Intelligence · · cited 5× · DOI ↗ · more like this ·

The functional programming community has developed a number of powerful abstractions for dealing with diverse programming models in a modular way. Beginning with a core of pure, side effect free computation, modular monadic semantics (MMS) allows designers to construct domain-specific languages by adding layers of semantic features, such as mutable state and I/O, in an a' la carte fashion. In the realm of interpreter and compiler construction, the benefits of this approach are manifold and well explored. This paper advocates bringing the tools of MMS to bear on hardware design and verification. In particular, we shall discuss a prototype compiler called ReWire which translates high-level MMS hardware specifications into working circuits on FPGAs. This enables designers to tackle the complexity of hardware design in a modular way, without compromising efficiency.

Making monads first-class with template haskell

Pericles S. Kariotis, Adam Procter, William L. Harrison

Artificial Intelligence · · cited 5× · DOI ↗ · more like this ·

Monads as an organizing principle for programming and semantics are notoriously difficult to grasp, yet they are a central and powerful abstraction in Haskell. This paper introduces a domain-specific language, MonadLab, that simplifies the construction of monads, and describes its implementation in Template Haskell. MonadLab makes monad construction truly first class, meaning that arcane theoretical issues with respect to monad transformers are completely hidden from the programmer. The motivation behind the design of MonadLab is to make monadic programming in Haskell simpler while providing a tool for non-Haskell experts that will assist them in understanding this powerful abstraction.

The Mechanized Marriage of Effects and Monads with Applications to High-assurance Hardware

Thomas N. Reynolds, Adam Procter, William L. Harrison +1 more

Artificial Intelligence · ACM Transactions on Embedded Computing Systems · · cited 4× · DOI ↗ · more like this ·

Constructing high-assurance, secure hardware remains a challenge, because to do so relies on both a verifiable means of hardware description and implementation. However, production hardware description languages (HDL) lack the formal underpinnings required by formal methods in security. Still, there is no such thing as high-assurance systems without high-assurance hardware. We present a core calculus of secure hardware description with its formal semantics, security type system, and mechanization in Coq. This calculus is the core of the functional HDL, ReWire, shown in previous work to have useful applications in reconfigurable computing. This work supports a full-fledged, formal methodology for producing high-assurance hardware.

Formal Semantics of Heterogeneous CUDA-C: A Modular Approach with Applications

Chris Hathhorn, Michela Becchi, William L. Harrison +1 more

cs.PL · · cited 3× · arXiv ↗ · more like this ·

We extend an off-the-shelf, executable formal semantics of C (Ellison and Rosu's K Framework semantics) with the core features of CUDA-C. The hybrid CPU/GPU computation model of CUDA-C presents challenges not just for programmers, but also for practitioners of formal methods. Our formal semantics helps expose and clarify these issues. We demonstrate the usefulness of our semantics by generating a tool from it capable of detecting some race conditions and deadlocks in CUDA-C programs. We discuss limitations of our model and argue that its extensibility can easily enable a wider range of verification tasks.

A core calculus for secure hardware

Thomas N. Reynolds, Adam Procter, William L. Harrison +1 more

Artificial Intelligence · · cited 1× · DOI ↗ · more like this ·

Constructing high assurance, secure hardware remains a challenge, because to do so relies on both a verifiable means of hardware description and implementation. However, production hardware description languages (HDL) lack the formal underpinnings required by formal methods in security. Still, there is no such thing as high assurance systems without high assurance hardware. We present a core calculus of secure hardware description with its formal semantics, security type system and mechanization in Coq. This calculus is the core of the functional HDL, ReWire, shown in previous work to have useful applications in reconfigurable computing. This work supports a full-fledged, formal methodology for producing high assurance hardware.

The Need for Delight in Online Education Materials

Adam Procter

Education · Electronic workshops in computing · · cited 1× · DOI ↗ · more like this ·

With the demand for online learning materials ever increasing and with more content being made open and free, Higher Education Institutes are now in a position to take their robust virtual learning environments and shift focus from content to user. The new objective being to provide a Delightful user experience that will not only surprise and excite but will improve education online.

DeepSim: Cluster Level Behavioral Simulation Model for Deep Learning

Yuankun Shi, Kevin Long, Kaushik Balasubramanian +3 more

Information Systems · · cited 0× · DOI ↗ · more like this ·

We are witnessing an explosion of AI based use cases driving the computer industry, and especially datacenter and server architectures. As Intel faces fierce competition in this emerging technology space, it is important that architecture definitions and directions are driven with data from proper tools and methodologies, and insights are drawn from end-to-end holistic analysis at the datacenter levels. In this paper, we introduce DeepSim, a cluster-level behavioral simulation model for deep learning. DeepSim, which is based on the Intel CoFluent simulation framework, uses timed behavioral models to simulate complex interworking between compute nodes, networking, and storage at the datacenter level, providing a realistic performance model of a real-world image recognition applications based on the popular Deep Learning Framework Caffe. The end-to-end simulation data from DeepSim…

This work is licensed under the Creative Commons Attribution License. Formal Semantics of Heterogeneous CUDA-C: A Modular Approach with Applications

F. Cassez, R. Huuck, G. Klein +5 more

Artificial Intelligence · · cited 0× · OpenAlex ↗ · more like this ·

We extend an off-the-shelf, executable formal semantics of C (Ellison and Ros,u’s K Framework se-mantics) with the core features of CUDA-C. The hybrid CPU/GPU computation model of CUDA-C presents challenges not just for programmers, but also for practitioners of formal methods. Our for-mal semantics helps expose and clarify these issues. We demonstrate the usefulness of our semantics by generating a tool from it capable of detecting some race conditions and deadlocks in CUDA-C programs. We discuss limitations of our model and argue that its extensibility can easily enable a wider range of verification tasks. 1

Node-Level Runtime System to Support Multi-tenancy in Clusters with GPUs

Michela Becchi, Kittisak Sajjapongse, Ian Graves +3 more

Hardware and Architecture · · cited 0× · OpenAlex ↗ · more like this ·

In the last few years, thanks to their computational power, their progressively increased programmability and their wide adoption in both the research community and the industry, GPUs have become part of HPC clusters (for example, the Chinese Tianhe-1A and the US Stampede supercomputers). As a result, widely used open-source cluster resource managers (e.g. SLURM and TORQUE) have recently been extended with GPU support capabilities. These systems, however, provide simple scheduling mechanisms that often result in resource underutilization and, thereby, in suboptimal performance. We propose a runtime system that provides abstraction and sharing of GPUs, while allowing isolation of concurrent applications. A central component of our runtime is a memory manager that provides a virtual memory abstraction to the applications. Our runtime is flexible in terms of scheduling policies, and allows…

H&S Reminders

Adam Procter

Artificial Intelligence · · cited 0× · OpenAlex ↗ · more like this ·

Screencast and related documents and links on general H&S reminders at WSA. This is a document to review just before the start of Semester 2 when our students work almost exclusively on Self Initiated project and Final Major Project.

User Experience (a hidden barrier) in OER

Adam Procter

Computer Science Applications · EdShare Southampton (University of Southampton) · · cited 0× · OpenAlex ↗ · more like this ·

More Open Education Resources (OER) and learning environments are being created and starting to mature and there are a number of barriers to learning and creator participation. One often overlooked barrier that has been given less attention, especially within OERs, is user experience (UX). UX is the way a person feels about using a product, system or service. We are creatures with emotional needs and, in the rush to get great content open and available sometimes the usability, the wow factor and good design principles get left by the wayside. I will demonstrate ways to think about UX for your OER and learning environments and why this is an important factor in helping engage learners with our educational materials.
\n‘The real payoff comes when we can make that remarkability last. When we can make people continually feel our work is worthy of discussion. When—for weeks, months…

Connected to Shared Drive Video demo

Adam Procter

Computer Networks and Communications · EdShare Southampton (University of Southampton) · · cited 0× · OpenAlex ↗ · more like this ·

Staff only video on connecting to WSA Shared from a Mac.
\n
\n***Note you must be on a secure connection - this means either a wired (ethernet) cable at work or connected to VPN for VPN support call Serviceline.
\n
\n
\n

General Terms

Pericles S. Kariotis, Adam M. Procter, William L. Harrison

Artificial Intelligence · · cited 0× · OpenAlex ↗ · more like this ·

Monads as an organizing principle for programming and semantics are notoriously difficult to grasp, yet they are a central and powerful abstraction in Haskell. This paper introduces a domain-specific language, MonadLab, that simplifies the construction of monads, and describes its implementation in Template Haskell. MonadLab makes monad construction truly first class, meaning that arcane theoretical issues with respect to monad transformers are completely hidden from the programmer. The motivation behind the design of MonadLab is to make monadic programming in Haskell simpler while providing a tool for non-Haskell experts that will assist them in understanding this powerful abstraction.

Web 2.0 for Creatives

Adam Procter

Computer Science Applications · EdShare Southampton (University of Southampton) · · cited 0× · OpenAlex ↗ · more like this ·

What is web 2.0, it is a Marketing term and can mean as little or as much as you want, we will be talking about Web 2.0 in terms of using current web technologies not only for the web but for other types of design.

Digital Printing and PDF creation

Adam Procter

Information Systems · EdShare Southampton (University of Southampton) · · cited 0× · OpenAlex ↗ · more like this ·

Short videos and Guides on how to print to various devices at WSA. Why 300dpi is important for printing, why PDF's are the defacto standard for printing and the how and where to get your files printed.

Blackboard Blogging & beyond

Adam Procter, Wsa Technical Services

Information Systems · · cited 0× · OpenAlex ↗ · more like this ·

This Share contains videos and links to help you get up to speed with blogging using Blackboard, Blackboard blogs are nice safe places to start blogging and although they don't look cool, there alright ! Then check out tumblr, wordpress or blogger to start blogging on your own in public !