A Type-System for describing System-on-a-Chip Architectures – Jan De Muijnck-Hughes

Title:
A Type-System for describing System-on-a-Chip Architectures

Abstract:
The protocols that describe the interactions between IP Cores on System-on-a-Chip (SoC) architectures are well-documented. These protocols described not only the structural properties of the physical interfaces but also the behaviour of the emanating signals. However, there is a disconnect between the design of SoC architectures, their formal description, and the verification of their implementation in known hardware description languages.

Within the Border Patrol project we are investigating how to capture and reason about the structural and behavioural properties of SoC architectures using state-of-the-art advances in programming language research. Namely, we are investigating using dependent types and session types to capture and reason about hardware communication.

In this talk I will discuss my work in designing a dependent type- system and corresponding language that captures and reasons about the topological structure of a System-on-a-Chip. This language provides correct-by-construction guarantees over:

  • the physical structure of an interaction protocol;
  • the adherence of a component’s interface to a given protocol; and
  • the validity of the specified connections made between components.

We provide these guarantees through the (ab)use of dependent types as presented in Idris; and abuse of indexed monads to reason about resource usage.

Given time I will give an account of how this language enables reasoning about SoC behaviour when considered in conjunction with Session Types.ssion Types.

Event details

  • When: 5th April 2018 12:00 - 13:00
  • Where: Cole 1.33a
  • Format: Talk

Diderot: A Parallel Domain-Specific Language for Image Analysis and Visualization – John Reppy

Diderot: A Parallel Domain-Specific Language for Image Analysis and Visualization

Abstract:
The analysis of structure in three-dimensional images is increasingly valuable for biomedical research and computational science. At the same time, the computational burden of processing images is increasing as devices produce images of higher resolution (e.g., typical CT scans have gone from 128^3 to roughly 512^3 resolutions). With the latest scanning technologies, it is also more common for the the values measured at each sample to be multi-dimensional rather than a single scalar, which further complicates implementing mathematically correct methods.

Diderot is a domain-specific language (DSL) for programming advanced 3D image visualization and analysis algorithms. These algorithms, such as volume rendering, fiber tractography, and particle systems, are naturally defined as computations over continuous tensor fields that are reconstructed from the discrete image data. Diderot combines a high-level mathematical programming notation based on tensor calculus with an abstract bulk-synchronous parallelism model. Diderot is designed to both enable rapid prototyping of new image analysis algorithms and high performance on a range of parallel platforms.

In this talk, I will give an overview of the design of Diderot and examples of its use. I will then describe aspects of its implementation with a focus on how we translate the notation of tensor calculus to efficient code. I will also briefly discuss the automated techniques we use to validate the correctness of the compilation process.

Diderot is joint work with Gordon Kindlmann, Charisee Chiw, Lamont Samuels, and Nick Seltzer.

Bio:
John Reppy is a Professor of Computer Science and a Senior Fellow of the Computation Institute at the University of Chicago. He received his Ph.D. from Cornell University in 1992 and spent the first eleven years of his career at Bell Labs in Murray Hill NJ. He has been exploring issues in language design and implementation since the late 1980’s, with a focus on higher-order, typed, functional languages. His work includes the invention of Concurrent ML and work on combining object-oriented and functional language features. His current research is on high-level languages for parallel programming, including the Diderot, Manticore, and Nessie projects.

Event details

  • When: 2nd April 2018 13:00 - 14:00
  • Where: Cole 1.33b
  • Format: Seminar

SRG Seminar: “On Engineering Unikernels” by Ward Jaradat

We have explored data coordination techniques that permit distributed systems to be constructed by interconnecting services. In such systems the network latency is often a problem. For example, large data volumes might have to be transmitted across the network if computation cannot be co-located close to data sources. One solution to this problem is the ability to deploy services in appropriate geographical locations and compose them together to create distributed ecosystems. Hence we seek to be able to deploy such services rapidly and dynamically enact and orchestrate them. However, this goal is hindered by the size of the deployments. Currently, virtual machine appliances that host such services on top of monolithic kernels are very large, thus are potentially slow to deploy as they may need to be transmitted across a network.

Our principles led us to take the route of re-engineering the standard software stack to create self-contained applications that are less-bloated and consequently much smaller based on Unikernels. Unikernels are compact library operating systems that enable a single application to be statically linked against a simple kernel that manages the underlying resources presented by a hypervisor. In this talk I will present Stardust – a specialised Unikernel that aims to support the deployment of application services based on the Java programming language.

Event details

  • When: 15th March 2018 13:00 - 14:00
  • Where: Cole 1.33b
  • Series: Systems Seminars Series
  • Format: Seminar

SACHI Seminar: Matjaž Kljun – Large scale studies of habit changing interface design

SACHI Seminar – Large scale studies of habit changing interface design

Speaker: Matjaž Kljun

Abstract:

Various technologies can be used in persuading people to change their habits, behaviours or attitudes. Such technologies are defined as persuasive and they are used in a variety of fields such as marketing, public health and education.

We are daily exposed to persuasion through different visualizations and triggers on all our devices. For example, a social networking application tries to persuade us in opening the app with a push notification and once the app is opened other hooks are placed so we spend more time in it. However, such applications are usually installed by us and we are inclined in using them. But could we persuade highly busy professionals in completing a training course or just about everybody to read terms of service? We will discuss these issues through large-scale studies that have been in done in the wild.

Speaker biography:  Matjaž Kljun is an assistant professor at the Faculty of Mathematics, Natural Sciences and Information Technologies at University of Primorska and is co-directing the HICUP lab (Humans Interacting with Computers at University of Primorska) and a research associate at the Faculty of Information studies, Slovenia. He received his Ph.D. degree in computer science from Lancaster University, UK. His research interests span across various fields related to Human-Computer Interaction, Personal Information Management and the use of technologies in teaching and learning.

Event details

  • When: 12th April 2018 14:00 - 15:00
  • Where: Cole 1.33b
  • Format: Seminar

SACHI Seminar: Klen Čopič Pucihar – The Missing Interface: Micro Gestures on Objects for Augmented Reality Interaction

SACHI Seminar – The Missing Interface: Micro Gestures on Objects for Augmented Reality Interaction

Speaker: Klen Čopič Pucihar

Abstract:

Augmented reality technology can introduce digital elements to arbitrary objects. However, these objects were never designed to incorporate the digital component, hence do not provide the necessary interface. To overcome this limitation, AR Interaction systems add sensors to objects, use additional handheld hardware or perform hand and body tracking. These methods are not optimal for direct interaction with physical objects  because they:

  • require modification of existing objects,
  • require the the user to hold the controller in their hand,
  • are based on synthesis of captured RGB or RGB-D data streams imposing the following limitations: (i) gestures need to be performed within the view of the camera; (ii) the gestures include reasonable large hand or finger movements (e.g. pinching the fingers, blooming gesture of opening the palm; (iii) the hand performing gesture is not occluded (e.g. cannot detect gestures if performed whilst grasping an object).

In this talk Klen will look at alternative methods which try to overcome such limitations and make inconspicuous, precise and flexible object oriented interaction possible for both augmented and mediated reality applications.

Speaker Biography

Klen Čopič Pucihar is assistant professor at the Faculty of Mathematics, Natural Sciences and Information Technologies at University of Primorska. Klen’s research vision is to look for new ways in which one could augmented, modify and mediate rich sources of visual, auditory and tactile stimuli that fabricate our everyday life experiences. The goal is to augment human abilities with new ways of using computational resources. This is important because the interface presents itself as the bottleneck between us humans and the benefit ever increasing computational resources could have on our everyday life. This makes the interfaces the core challenge for the future and the essence of Klen’s research which is currently mainly concentrated on augmented reality, mobile computing and human-computer interaction focusing on different perceptual issues that arise whilst interacting with various computer systems which lead to innovative user interface designs. Klen’s work was published as high ranked scientific publications and won him best poster award at ISMAR 2014.

Event details

  • When: 12th April 2018 14:00 - 15:00
  • Where: Cole 1.33b
  • Format: Seminar

Marwan Fayed (St Andrews): Quality of Experience Fairness for Adaptive Video Streams in the Network (School Seminar)

Abstract:

“Why is my kid getting HD on their phone, while I’m stuck with SD on my 50″ TV?” This type of complaint is among the most common directed to streaming services such as Netflix and BBC. Recent studies observe that adaptive video streams, when competing behind a bottleneck link, generate flows that lead to instability, under-utilization, and unfairness. Additional measurements suggest there may also be a negative impact on users’ perceived quality of experience as a consequence. The intuitive response may be, and has been, that application-generated issues should be resolved by the application. In this presentation I shall demonstrate that fairness, by any definition, can only be solved in the network. Moreover, that in an increasingly HTTP-S world, some form of client interaction is required. In support, a new network-layer ‘QoE-fairness’ metric will be be introduced that reflects user experience. Experiments using our open-source implementation in the home environment reinforce the network-layer as the right place to attack the general problem.

Refs-

[1] http://dl.ifip.org/db/conf/networking/networking2015/1570066341.pdf
[2] https://dl.acm.org/citation.cfm?id=2940144

Speaker Bio:
Marwan Fayed joined the University of St Andrews in 2018. He received his MA from Boston University and his PhD from the University of Ottawa, in 2003 and 2009 respectively, and in between worked at Microsoft as a member of the Core Reliability Group. In 2009 he joined the University of Stirling, UK as Scottish Informatics and Computer Science Alliance (SICSA) Lecturer, alongside an appointment to ‘Theme Leader’ for networking research in Scotland, 2014-2016. His current research interests lie in wireless algorithms, as well as general network, transport, and measurement in next generation edge networks. He is a co-founder of HUBS C.i.C., an ISP focussed on rural communities, recipient of an IEEE best paper award, and a Senior Member of both the IEEE and ACM.

Event details

  • When: 17th April 2018 14:00 - 15:00
  • Where: Cole 1.33a
  • Series: School Seminar Series
  • Format: Seminar

Compositional Coinduction with Sized Types – Dr. Andreas Abel

Abstract:

Formal languages and automata are taught to every computer science student.  However, the student will most likely not see the beautiful coalgebraic foundations, which use coindutive reasoning.

In this talk, I recapitulate how infinite tries can represent formal languages (sets of strings).  I explain Agda’s coinduction mechanism based on copatterns and sized types demonstrate that it allows an elegant representation of the usual language constructions like union, concatenation, and Kleene star, with the help of Brzozowski derivatives.

Event details

  • When: 16th February 2018 12:00 - 13:00
  • Where: Cole 1.33b
  • Format: Seminar

Impact Talk: Xelect Ltd

This is Impact talk as a “brown bag lunch” (i.e. you bring your lunch if you wish) and the school will provide cakes.

Xelect Ltd

– a successful spin-out from the University of St Andrews

Xelect was founded 5 years ago by Professor Ian Johnston and Dr Tom Ashton to provide genetic services to the global aquaculture industry. The company built on several decades of research in fish physiology and genetics which was funded by BBSRC through to the stage of commercialisation. Xelect develops genetic selection technology and provides associated laboratory support to breeders of finfish, shellfish and shrimps and to date has served 52 customers in 17 countries. We currently manage broodstock genetics programs for producers in Chile, Scotland (Atlantic salmon), Croatia, Greece (seabass and sea bream), New Zealand (King salmon) and Vietnam (Barramundi). The company started out in incubation space at the Scottish Oceans Institute before moving to independent premises in 2016. Xelect also has sales offices in Puerto Montt, Chile and in Hong Kong. The company employs 12 people, mostly PhDs, and is account managed by Scottish Enterprise. Xelect’s shareholders are the founders, the University, SalmoBreed A/S and the EOS Technology Investment Syndicate.

About Ian Johnston

Ian Johnston is former Chandos Professor, Head of the School of Biology and Director of the Scottish Oceans Institute. He currently works full-time for Xelect but retains a 0 FTE position as Professor of Biology.

Event details

  • When: 8th February 2018 13:00 - 14:00
  • Where: Cole 1.33a
  • Format: Seminar, Talk

Simplifying ARM concurrency – Prof. Susmit Sarkar

ARM has a relaxed memory model, previously specified in informal prose for ARMv7 and ARMv8. Over time, and partly due to work building formal semantics for ARM concurrency, it has become clear that some of the complexity of the model is not justified by the potential benefits. In
particular, the model was originally non-multicopy-atomic: writes could
become visible to some other threads before becoming visible to all —
but this has not been exploited in production implementations, the
corresponding potential hardware optimisations are thought to have
insufficient benefits in the ARM context, and it gives rise to subtle
complications when combined with other ARMv8 features. The ARMv8
architecture has therefore been revised: it now has a multicopy-atomic
model. It has also been simplified in other respects, including more
straightforward notions of dependency, and the architecture now includes
a formal concurrency model.

This is work presented in POPL this year. I will also present some of
the background and context on relaxed memory which is absent from the
necessarily compressed talk format of POPL.

Event details

  • When: 22nd February 2018 12:00 - 13:00
  • Where: Cole 1.33a
  • Format: Talk