A Revisionist History of Concurrent Separation Logic

We present TaDA Live, a concurrent separation logic for reasoning compositionally about the termination of blocking fine-grained concurrent programs. The crucial challenge is how to deal with abstract atomic blocking : that is, abstract atomic operations that have blocking behaviour arising from busy-waiting patterns as found in, for example, fine-grained spin locks. Our fundamental innovation is with the design of abstract specifications that capture this blocking behaviour as liveness assumptions on the environment. We design a logic that can reason about the termination of clients that use such operations without breaking their abstraction boundaries, and the correctness of the implementations of the operations with respect to their abstract specifications. We introduce a novel semantic model using layered subjective obligations to express liveness invariants and a proof system that is sound with respect to the model. The subtlety of our specifications and reasoning is illustrated using several case studies.

Download Full-text

Short Fictions of Improvement by James Hogg and Walter Scott

Dialectics of Improvement ◽

10.3366/edinburgh/9781474441674.003.0003 ◽

2020 ◽

pp. 72-111

Author(s):

Gerard Lee McKeever

Keyword(s):

Short Fiction ◽

Formal Logic ◽

Literary Marketplace ◽

James Hogg ◽

Wide Range ◽

Revisionist History ◽

History Of ◽

Walter Scott ◽

Selection Of ◽

Half Decade

This chapter reads James Hogg and Walter Scott within a new, revisionist history of short fiction that is particularly interested in the genre of the ‘tale’. Focusing on the half-decade between 1827 and 1831, the chapter highlights a selection of Hogg’s mature contributions to Blackwood’s Edinburgh Magazine alongside Scott’s Chronicles of the Canongate (first series). These years were marked by literary experimentation, when a confident improving persuasion in Scottish culture was threatening to unravel. The formal logic of these short fictions, defined by a curiously focused spontaneity, exacerbates a pluralistic handling of the collision between improvement and tradition. Different models of time (progress, renewal, disruption) and belief (suspension, scepticism, credulity) serve to interrogate improvement in a wide range of contexts around commercial modernisation. The chapter unpacks two specific literary innovations in this context. The first looks to acts of transmission in the literary marketplace which by turns sustain, contain and defer the dialectics of improvement. The second sees the emergence of a fully fledged aesthetic vocabulary of culture in Scott’s writing.

Download Full-text

Granularity and Concurrent Separation Logic

CONCUR 2011 – Concurrency Theory - Lecture Notes in Computer Science ◽

10.1007/978-3-642-23217-6_15 ◽

2011 ◽

pp. 219-234 ◽

Cited By ~ 1

Author(s):

Jonathan Hayman

Keyword(s):

Separation Logic ◽

Concurrent Separation Logic

Download Full-text

The creation of thermodynamics

Block by Block: The Historical and Theoretical Foundations of Thermodynamics ◽

10.1093/oso/9780198851547.003.0033 ◽

2020 ◽

pp. 422-437

Author(s):

Robert T. Hanlon

Keyword(s):

The North ◽

Revisionist History ◽

History Of ◽

The Creation ◽

Written Word ◽

Definition Of ◽

John Tyndall

The North British group of scientists, including Thomson, Rankine, an adopted Joule, Tait, and Maxwell created in the written word the field of thermodynamics in which temperature plays a central role. Thomson experienced the first glimpse of dQ/T; however, a valid definition of the 2nd Law of Thermodynamics remained absent. John Tyndall challenged the revisionist history of this group in which Joule was declared the first to discover heat–work equivalence and not the German Mayer. This led to the infamous Tait–Tyndall controversy.

Download Full-text