Publications related to Verification of STM on relaxed memory models

Degrees of Separation: A Flexible Type System for Safe Concurrency

Martin Odersky, Aleksander Slawomir Boruch-Gruszecki, Yichen Xu

Data races have long been a notorious problem in concurrent programming. They are subtle to detect, and lead to non-deterministic behaviours. There has been a lot of interest in type systems that statically guarantee data race freedom. Significant progress ...

2024

EdgeAI-Aware Design of In-Memory Computing Architectures

Marco Antonio Rios

Driven by the demand for real-time processing and the need to minimize latency in AI algorithms, edge computing has experienced remarkable progress. Decision-making AI applications stand out for their heavy reliance on data-centric operations, predominantl ...

EPFL2024

Automated Formal Verification of Software Network Functions

Solal Vincenzo Pirelli

Formally verifying the correctness of software is necessary to merit the trust people put in software systems. Currently, formal verification requires human effort to prove that a piece of code matches its specification and code changes to improve verifiab ...

EPFL2024

Bit-Line Computing for CNN Accelerators Co-Design in Edge AI Inference

David Atienza Alonso, Giovanni Ansaloni, Alexandre Sébastien Julien Levisse, Flavio Ponzina, Marco Antonio Rios

By supporting the access of multiple memory words at the same time, Bit-line Computing (BC) architectures allow the parallel execution of bit-wise operations in-memory. At the array periphery, arithmetic operations are then derived with little additional o ...

2023

Building Chips Faster: Hardware-Compiler Co-Design for Accelerated RTL Simulation

Sahand Kashani

The demise of Moore's Law and Dennard scaling has resulted in diminishing performance gains for general-purpose processors, and so has prompted a surge in academic and commercial interest for hardware accelerators. Specialized hardware has already redefine ...

EPFL2023

Chaosity: Understanding Contemporary NUMA-architectures

Anastasia Ailamaki, Viktor Sanca, Syed Mohammad Aunn Raza, Hamish Mcniece Hill Nicholson, Andreea Nica

Modern hardware is increasingly complex, requiring increasing effort to understand in order to carefully engineer systems for optimal performance and effective utilization. Moreover, established design principles and assumptions are not portable to modern ...

2023

Bodily self-consciousness as a framework to link sensory information and self-related components of episodic memory: behavioral, neuroimaging, and clinical evidence

Nathalie Heidi Meyer

The recollection of sensory information and subjective experience related to a personal past event depends on our episodic memory (EM). At the neural level, EM retrieval is linked with the reinstatement of hippocampal activity thought to recollect the sens ...

EPFL2023

Computational models of episodic-like memory in food-caching birds

Wulfram Gerstner, Johanni Michael Brea

How the 'what', 'where', and 'when' of past experiences are stored in episodic memories and retrieved for suitable decisions remains unclear. In an effort to address these questions, the authors present computational models of neural networks that behave l ...

Nature Portfolio2023

Imprecise Store Exceptions

Babak Falsafi, Siddharth Gupta, Mathias Josef Payer, Yunho Oh, Yuanlong Li, Qingxuan Kang, Abhishek Bhattacharjee

Precise exceptions are a cornerstone of modern computing as they provide the abstraction of sequential instruction execution to programmers while accommodating microarchitectural optimizations. However, increasing compute capabilities in deep memory hierar ...

ACM2023

A theory of memory consolidation and synaptic pruning in cortical circuits

Georgios Iatropoulos

Over the course of a lifetime, the human brain acquires an astonishing amount of semantic knowledge and autobiographical memories, often with an imprinting strong enough to allow detailed information to be recalled many years after the initial learning exp ...

EPFL2023

HetCache: Synergising NVMe Storage and GPU acceleration for Memory-Efficient Analytics

Anastasia Ailamaki, Periklis Chrysogelos, Syed Mohammad Aunn Raza, Hamish Mcniece Hill Nicholson

Accessing input data is a critical operation in data analytics: i) slow data access significantly degrades performance, and ii) storing everything in the fastest medium, i.e., memory, incurs high operational and hardware costs. Further, while GPUs offer in ...

2023

Automating the Design of Programmable Interconnect for Reconfigurable Architectures

Stefan Nikolic

With Moore's law coming to an end, increasingly more hope is being put in specialized hardware implemented on reconfigurable architectures such as Field-Programmable Gate Arrays (FPGAs). Yet, it is often neglected that these architectures themselves experi ...

EPFL2023

In-Memory Hardware and Architectural Extensions for Workloads Acceleration

William Andrew Simon

Utilization of edge devices has exploded in the last decade, with such use cases as wearable devices, autonomous driving, and smart homes. As their ubiquity grows, so do expectations of their capabilities. Simultaneously, their formfactor and use cases lim ...

EPFL2022

Decentralized in-order execution of a sequential task-based code for shared-memory architectures

Charly Nicolas Lucien Castes

The hardware complexity of modern machines makes the design of adequate programming models crucial for jointly ensuring performance, portability, and productivity in high-performance computing (HPC). Sequential task-based programming models paired with adv ...

IEEE COMPUTER SOC2022

Kernel Memory Networks: A Unifying Framework for Memory Modeling

Wulfram Gerstner, Georgios Iatropoulos, Johanni Michael Brea

We consider the problem of training a neural network to store a set of patterns with maximal noise robustness. A solution, in terms of optimal weights and state update rules, is derived by training each individual neuron to perform either kernel classifica ...

Curran Associates2022

Modulation of working memory duration by synaptic and astrocytic mechanisms

Sophia Becker

Short-term synaptic plasticity and modulations of the presynaptic vesicle release rate are key components of many working memory models. At the same time, an increasing number of studies suggests a potential role of astrocytes in modulating higher cognitiv ...

PUBLIC LIBRARY SCIENCE2022

Where does the engram come from? Study of prefrontal cortex inputs during memory consolidation

Lucie Pauline Dixsaut

The formation and storage of memories has been under deep investigation for several decades. Nevertheless, the precise contribution of each brain region involved in this process and the interplay between them across memory consolidation is still largely de ...

EPFL2022

Scaling Language Features for Program Verification

Georg Stefan Schmid

Formal verification of real-world software systems remains challenging for a number of reasons, including lack of automation, friction in specifying properties, and limited support for the diverse programming paradigms used in industry. In this thesis we m ...

EPFL2022

Inter-actions parallel execution on GPU from high-level dataflow synthesis

Marco Mattavelli, Simone Casale Brunet, Aurélien François Gilbert Bloch

Recent GPU architectures make available numbers of parallel processing units that exceed by orders of magnitude the ones offered by CPU architectures. Whereas programs written using dataflow programming languages are well suited for programming heterogeneo ...

IEEE2022

Structure-preserving approaches and data-driven closure modeling for model order reduction

Nicolò Ripamonti

In this thesis, we propose model order reduction techniques for high-dimensional PDEs that preserve structures of the original problems and develop a closure modeling framework leveraging the Mori-Zwanzig formalism and recurrent neural networks. Since high ...

EPFL2022