Zobrazeno 1 - 10
of 419
pro vyhledávání: '"Lahav, Ori"'
Programs written in C/C++ often include inline assembly: a snippet of architecture-specific assembly code used to access low-level functionalities that are impossible or expensive to simulate in the source language. Although inline assembly is widely
Externí odkaz:
http://arxiv.org/abs/2408.17208
Reasoning about hyperproperties of concurrent implementations, such as the guarantees these implementations provide to randomized client programs, has been a long-standing challenge. Standard linearizability enables the use of atomic specifications f
Externí odkaz:
http://arxiv.org/abs/2408.11015
CXL (Compute Express Link) is an emerging open industry-standard interconnect between processing and memory devices that is expected to revolutionize the way systems are designed in the near future. It enables cache-coherent shared memory pools in a
Externí odkaz:
http://arxiv.org/abs/2407.16300
We present a general methodology for establishing the impossibility of implementing certain concurrent objects on different (weak) memory models. The key idea behind our approach lies in characterizing memory models by their mergeability properties,
Externí odkaz:
http://arxiv.org/abs/2405.16611
Autor:
Wu, Haoze, Isac, Omri, Zeljić, Aleksandar, Tagomori, Teruhiro, Daggitt, Matthew, Kokke, Wen, Refaeli, Idan, Amir, Guy, Julian, Kyle, Bassan, Shahaf, Huang, Pei, Lahav, Ori, Wu, Min, Zhang, Min, Komendantskaya, Ekaterina, Katz, Guy, Barrett, Clark
This paper serves as a comprehensive system description of version 2.0 of the Marabou framework for formal analysis of neural networks. We discuss the tool's architectural design and highlight the major features and components introduced since its in
Externí odkaz:
http://arxiv.org/abs/2401.14461
Software Transactional Memory (STM) is an extensively studied paradigm that provides an easy-to-use mechanism for thread safety and concurrency control. With the recent advent of byte-addressable persistent memory, a natural question to ask is whethe
Externí odkaz:
http://arxiv.org/abs/2312.13828
Rely-guarantee (RG) is a highly influential compositional proof technique for concurrent programs, which was originally developed assuming a sequentially consistent shared memory. In this paper, we first generalize RG to make it parametric with respe
Externí odkaz:
http://arxiv.org/abs/2305.08486
The rise of persistent memory is disrupting computing to its core. Our work aims to help programmers navigate this brave new world by providing a program logic for reasoning about x86 code that uses low-level operations such as memory accesses and fe
Externí odkaz:
http://arxiv.org/abs/2201.05860
Autor:
Khyzha, Artem, Lahav, Ori
We study abstraction for crash-resilient concurrent objects using non-volatile memory (NVM). We develop a library correctness criterion that is sound for ensuring contextual refinement in this setting, thus allowing clients to reason about library be
Externí odkaz:
http://arxiv.org/abs/2111.03881
Publikováno v:
In Aquaculture Reports June 2024 36
