Zobrazeno 1 - 10
of 34
pro vyhledávání: '"Colvin, Robert J."'
Autor:
Colvin, Robert J., Hayes, Ian J., Heiner, Scott, Höfner, Peter, Meinicke, Larissa, Su, Roger C.
Developers of low-level systems code providing core functionality for operating systems and kernels must address hardware-level features of modern multicore architectures. A particular feature is pipelined "out-of-order execution" of the code as writ
Externí odkaz:
http://arxiv.org/abs/2407.20559
Autor:
Colvin, Robert J.
The C/C++ memory model provides an interface and execution model for programmers of concurrent (shared-variable) code. It provides a range of mechanisms that abstract from underlying hardware memory models -- that govern how multicore architectures h
Externí odkaz:
http://arxiv.org/abs/2204.03189
Autor:
Colvin, Robert J.
Since the introduction of the CDC 6600 in 1965 and its `scoreboarding' technique processors have not (necessarily) executed instructions in program order. Programmers of high-level code may sequence independent instructions in arbitrary order, and it
Externí odkaz:
http://arxiv.org/abs/2105.02444
Autor:
Colvin, Robert J., Winter, Kirsten
Reasoning about correctness and security of software is increasingly difficult due to the complexity of modern microarchitectural features such as out-of-order execution. A class of security vulnerabilities termed Spectre that exploits side effects o
Externí odkaz:
http://arxiv.org/abs/2004.00577
Autor:
Colvin, Robert J., Smith, Graeme
Modern processors deploy a variety of weak memory models, which for efficiency reasons may execute instructions in an order different to that specified by the program text. The consequences of instruction reordering can be complex and subtle, and can
Externí odkaz:
http://arxiv.org/abs/1812.00996
Publikováno v:
EPTCS 282, 2018, pp. 53-67
In this paper we develop a theory for correctness of concurrent objects under weak memory models. Central to our definitions is the concept of observations which determine when effects of operations become visible, and hence determine the semantics o
Externí odkaz:
http://arxiv.org/abs/1810.09612
Linearizability is a widely accepted notion of correctness for concurrent objects. Recent research has investigated redefining linearizability for particular hardware weak memory models, in particular for TSO. In this paper, we provide an overview of
Externí odkaz:
http://arxiv.org/abs/1802.04954
Autor:
Colvin, Robert J., Smith, Graeme
Modern processors deploy a variety of weak memory models, which for efficiency reasons may (appear to) execute instructions in an order different to that specified by the program text. The consequences of instruction reordering can be complex and sub
Externí odkaz:
http://arxiv.org/abs/1802.04406
A synchronous program algebra: a basis for reasoning about shared-memory and event-based concurrency
This research started with an algebra for reasoning about rely/guarantee concurrency for a shared memory model. The approach taken led to a more abstract algebra of atomic steps, in which atomic steps synchronise (rather than interleave) when compose
Externí odkaz:
http://arxiv.org/abs/1710.03352
A wide-spectrum language integrates specification constructs into a programming language in a manner that treats a specification command just like any other command. This paper investigates a semantic model for a wide-spectrum language that supports
Externí odkaz:
http://arxiv.org/abs/1609.00195