Publications associées à Formalizing and verifying transactional memories

Oligolithic Cross-task Optimizations across Isolated Workloads

Anastasia Ailamaki, Panagiotis Sioulas, Eleni Zapridou

Enterprises collect data in large volumes and leverage them to drive numerous concurrent decisions and business processes. Their teams deploy multiple applications that often operate concurrently on the same data and infrastructure but have widely differen ...

2024

Driving and suppressing the human language network using large language models

Martin Schrimpf

Transformer models such as GPT generate human-like language and are predictive of human brain responses to language. Here, using functional-MRI-measured brain responses to 1,000 diverse sentences, we first show that a GPT-based encoding model can predict t ...

Nature Portfolio2024

Formal Foundations of Capture Tracking

Aleksander Slawomir Boruch-Gruszecki

Type systems are a device for verifying properties of programs without running them. Many programming languages used in the industry have always had a type system, while others were initially created without a type system and later adopted one, when the ad ...

EPFL2024

Secure Interface Design Leveraging Hardware/Software Support

Atri Bhattacharyya

Computer systems rely heavily on abstraction to manage the exponential growth of complexity across hardware and software. Due to practical considerations of compatibility between components of these complex systems across generations, developers have favou ...

EPFL2024

The conceptual foundations of innate immunity: Taking stock 30 years later

Bruno Lemaitre

While largely neglected over decades during which adaptive immunity captured most of the attention, innate immune mechanisms have now become central to our understanding of immunology. Innate immunity provides the first barrier to infection in vertebrates, ...

2024

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

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

Orthologic with Axioms

Viktor Kuncak, Simon Guilloud

We study the proof theory and algorithms for orthologic, a logical system based on ortholattices, which have shown practical relevance in simplification and normalization of verification conditions. Ortholattices weaken Boolean algebras while having polyno ...

Association for Computing Machinery2024

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

One-shot Garbage Collection for In-memory OLTP through Temporality-aware Version Storage

Anastasia Ailamaki, Angelos Christos Anadiotis, Periklis Chrysogelos, Syed Mohammad Aunn Raza

Most modern in-memory online transaction processing (OLTP) engines rely on multi-version concurrency control (MVCC) to provide data consistency guarantees in the presence of conflicting data accesses. MVCC improves concurrency by generating a new version o ...

ACM2023

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

2D Nanosystems: Applications of 2D Semiconductors for In-Memory Computing

Guilherme Migliato Marega

Machine learning and data processing algorithms have been thriving in finding ways of processing and classifying information by exploiting the hidden trends of large datasets. Although these emerging computational methods have become successful in today's ...

EPFL2023

Type-Preserving Compilation of Class-Based Languages

Guillaume André Fradji Martres

The Dependent Object Type (DOT) calculus was designed to put Scala on a sound basis, but while DOT relies on structural subtyping, Scala is a fundamentally class-based language. This impedance mismatch means that a proof of DOT soundness by itself is ...

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

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

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

How to Achieve Large-Area Ultra-Fast Operation of MoS 2 Monolayer Flash Memories?

Andras Kis, Aleksandra Radenovic, Yanfei Zhao, Zhenyu Wang, Guilherme Migliato Marega, Mukesh Kumar Tripathi, Hyungoo Ji, Asmund Kjellegaard Ottesen

Memory devices have returned to the spotlight due to increasing interest in using in-memory computing architectures to make data-driven algorithms more energy-efficient. One of the main advantages of this architecture is the efficient performance of vector ...

2023

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

Rebooting Virtual Memory with Midgard

Siddharth Gupta

Virtual Memory (VM) is a critical programming abstraction that is widely used in various modern computing platforms. With the rise of datacenter computing and birth of planet-scale online services, the semantic and capacity requirements from memory have ev ...

EPFL2023

The splay-list: a distribution-adaptive concurrent skip-list

Dan Alistarh, Amirkeivan Mohtashami

The design and implementation of efficient concurrent data structures has seen significant attention. However, most of this work has focused on concurrent data structures providing good worst-case guarantees, although, in real workloads, objects are often ...

SPRINGER2023