On the public citation graph

Weak persistency semantics from the ground up: formalising the persistency semantics of ARMv8 and transactional models

0 signed · 91 inferred · view as graph

Inferred edges come from two machine sources: sweeps of open repository metadata (mostly SSRN and Zenodo), and a bulk OpenAlex citation snapshot. Every row below is labelled with the one it came from. Neither is a complete citation index — absence here is not evidence of absence.

Is this your work? Sign in with ORCID and put your name on the claims that are yours.
Claim with ORCID
Reference health. See whether every reference in this work resolves to a known work and none has been retracted — and get a dated CiteStamped badge you can embed.
See reference health

What this work says

Outgoing claims: the papers this work cites, builds on, or argues with.

inferredcites →https://doi.org/10.1007/978-3-030-11245-5_1openalex-snapshot
On the Semantics of Snapshot Isolation
inferredcites →https://doi.org/10.1007/978-3-319-89884-1_33openalex-snapshot
On Parallel Snapshot Isolation and Release/Acquire Consistency
inferredcites →https://doi.org/10.1007/978-3-642-19835-9_5openalex-snapshot
Litmus: Running Tests against Hardware
inferredcites →https://doi.org/10.1007/978-3-662-48653-5_41openalex-snapshot
Hardware Transactions in Nonvolatile Memory
inferredcites →https://doi.org/10.1007/978-3-662-53426-7_23openalex-snapshot
Linearizability of Persistent Memory Objects Under a Full-System-Crash Failure Model
inferredcites →https://doi.org/10.1016/j.microrel.2011.09.028openalex-snapshot
Spin-transfer torque RAM technology: Review and prospect
inferredcites →https://doi.org/10.1038/nature06932openalex-snapshot
The missing memristor found
inferredcites →https://doi.org/10.1109/fccm.2018.00035openalex-snapshot
Microscope on Memory: MPSoC-Enabled Computer Memory System Assessments
inferredcites →https://doi.org/10.1109/micro.2016.7783761openalex-snapshot
Delegated persist ordering
inferredcites →https://doi.org/10.1109/nvmsa.2018.00015openalex-snapshot
Empirical Study of Transactional Management for Persistent Memory
inferredcites →https://doi.org/10.1109/tc.1979.1675439openalex-snapshot
How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Programs
inferredcites →https://doi.org/10.1145/1555754.1555758openalex-snapshot
Architecting phase change memory as a scalable dram alternative
inferredcites →https://doi.org/10.1145/1629575.1629589openalex-snapshot
Better I/O through byte-addressable, persistent memory
inferredcites →https://doi.org/10.1145/1785414.1785443openalex-snapshot
x86-TSO
inferredcites →https://doi.org/10.1145/1926385.1926394openalex-snapshot
Mathematizing C++ concurrency
inferredcites →https://doi.org/10.1145/1950365.1950379openalex-snapshot
Mnemosyne
inferredcites →https://doi.org/10.1145/1950365.1950380openalex-snapshot
NV-Heaps
inferredcites →https://doi.org/10.1145/1961296.1950380openalex-snapshot
NV-Heaps
inferredcites →https://doi.org/10.1145/2063384.2063436openalex-snapshot
SCMFS
inferredcites →https://doi.org/10.1145/2248487.1950379openalex-snapshot
Mnemosyne
inferredcites →https://doi.org/10.1145/2540708.2540744openalex-snapshot
Kiln
inferredcites →https://doi.org/10.1145/2694344.2694391openalex-snapshot
GPU Concurrency
inferredcites →https://doi.org/10.1145/2714064.2660224openalex-snapshot
Atlas
inferredcites →https://doi.org/10.1145/2830772.2830805openalex-snapshot
Efficient persist barriers for multicores
inferredcites →https://doi.org/10.1145/2872362.2872406openalex-snapshot
Specifying and Checking File System Crash-Consistency Models
inferredcites →https://doi.org/10.1145/2872362.2872410openalex-snapshot
Failure-Atomic Persistent Memory Updates via JUSTDO Logging
inferredcites →https://doi.org/10.1145/2926697.2926704openalex-snapshot
Persistence programming models for non-volatile memory
inferredcites →https://doi.org/10.1145/2954679.2872381openalex-snapshot
High-Performance Transactions for Persistent Memories
inferredcites →https://doi.org/10.1145/2994593openalex-snapshot
Don’t Sit on the Fence
inferredcites →https://doi.org/10.1145/3009837.3009838openalex-snapshot
Automatically comparing memory consistency models
inferredcites →https://doi.org/10.1145/3037697.3037723openalex-snapshot
Automated Synthesis of Comprehensive Memory Model Litmus Test Suites
inferredcites →https://doi.org/10.1145/3062341.3062352openalex-snapshot
Repairing sequential consistency in C/C++11
inferredcites →https://doi.org/10.1145/3079856.3080229openalex-snapshot
Language-level persistency
inferredcites →https://doi.org/10.1145/3158107openalex-snapshot
Simplifying ARM concurrency: multicopy-atomic axiomatic and operational models for ARMv8
inferredcites →https://doi.org/10.1145/3192366.3192367openalex-snapshot
Persistency for synchronization-free regions
inferredcites →https://doi.org/10.1145/3192366.3192373openalex-snapshot
The semantics of transactions and weak memory in x86, Power, ARM, and C++
inferredcites →https://doi.org/10.1145/322154.322158openalex-snapshot
The serializability of concurrent database updates
inferredcites →https://doi.org/10.1145/325096.325102openalex-snapshot
Memory consistency and event ordering in scalable shared-memory multiprocessors
inferredcites →https://doi.org/10.1145/3276507openalex-snapshot
Persistence semantics for weak memory: integrating epoch persistency with the TSO memory model
inferredcites →https://doi.org/10.1145/3290382openalex-snapshot
Bridging the gap between programming languages and hardware weak memory models
inferredcites →https://doi.org/10.1145/3297858.3304015openalex-snapshot
PMTest
inferredcites →https://doi.org/10.1145/78969.78972openalex-snapshot
Linearizability: a correctness condition for concurrent objects
inferredcites →https://doi.org/10.14778/2735479.2735483openalex-snapshot
REWIND
inferredcites →https://doi.org/10.4230/lipics.disc.2017.37openalex-snapshot
Dalí: A Periodically Persistent Hash Map

What points at this work

Incoming claims: where this work appears in other papers’ reference lists and arguments.

inferred← citeshttps://doi.org/10.1007/978-3-030-44914-8_23openalex-snapshot
ARMv8-A System Semantics: Instruction Fetch in Relaxed Architectures
inferred← citeshttps://doi.org/10.1007/978-3-030-50086-3_3openalex-snapshot
Defining and Verifying Durable Opacity: Correctness for Persistent Software Transactional Memory
inferred← citeshttps://doi.org/10.1007/978-3-030-92124-8_13openalex-snapshot
Checking Opacity and Durable Opacity with FDR
inferred← citeshttps://doi.org/10.1007/978-3-030-99336-8_9openalex-snapshot
View-Based Owicki–Gries Reasoning for Persistent x86-TSO
inferred← citeshttps://doi.org/10.1007/978-3-031-25803-9_6openalex-snapshot
SMT-Based Verification of Persistency Invariants of Px86 Programs
inferred← citeshttps://doi.org/10.1007/978-3-031-50521-8_2openalex-snapshot
A Fully Verified Persistency Library
inferred← citeshttps://doi.org/10.1007/978-3-031-57267-8openalex-snapshot
Programming Languages and Systems
inferred← citeshttps://doi.org/10.1007/978-3-031-57267-8_6openalex-snapshot
Intel PMDK Transactions: Specification, Validation and Concurrency
inferred← citeshttps://doi.org/10.1007/978-3-031-57267-8_8openalex-snapshot
Specifying and Verifying Persistent Libraries
inferred← citeshttps://doi.org/10.1007/978-3-031-91118-7_3openalex-snapshot
Sufficient Conditions for Robustness of RDMA Programs
inferred← citeshttps://doi.org/10.1007/978-3-031-92196-4_8openalex-snapshot
Self-powered Embedded Systems: The Role of Non-volatile Memory Technology in IoT Devices
inferred← citeshttps://doi.org/10.1007/s10703-024-00462-1openalex-snapshot
A verified durable transactional mutex lock for persistent x86-TSO
inferred← citeshttps://doi.org/10.1109/iccq51190.2021.9392904openalex-snapshot
An Efficient Dynamic Analysis Tool for Checking Durable Linearizability
inferred← citeshttps://doi.org/10.1109/isca45697.2020.00076openalex-snapshot
TransForm: Formally Specifying Transistency Models and Synthesizing Enhanced Litmus Tests
inferred← citeshttps://doi.org/10.1109/isca52012.2021.00043openalex-snapshot
Execution Dependence Extension (EDE): ISA Support for Eliminating Fences
inferred← citeshttps://doi.org/10.1145/3371079openalex-snapshot
Persistency semantics of the Intel-x86 architecture
inferred← citeshttps://doi.org/10.1145/3385412.3385991openalex-snapshot
Crafty: efficient, HTM-compatible persistent transactions
inferred← citeshttps://doi.org/10.1145/3385412.3386000openalex-snapshot
PMThreads: persistent memory threads harnessing versioned shadow copies
inferred← citeshttps://doi.org/10.1145/3385412.3386031openalex-snapshot
NVTraverse: in NVRAM data structures, the destination is more important than the journey
inferred← citeshttps://doi.org/10.1145/3428219openalex-snapshot
Persistent Owicki-Gries reasoning: a program logic for reasoning about persistent programs on Intel-x86
inferred← citeshttps://doi.org/10.1145/3428231openalex-snapshot
Towards a formal foundation of intermittent computing
inferred← citeshttps://doi.org/10.1145/3434328openalex-snapshot
Taming x86-TSO persistency
inferred← citeshttps://doi.org/10.1145/3434337openalex-snapshot
Deciding reachability under persistent x86-TSO
inferred← citeshttps://doi.org/10.1145/3445814.3446694openalex-snapshot
Hippocrates: healing persistent memory bugs without doing any harm
inferred← citeshttps://doi.org/10.1145/3453483.3454027openalex-snapshot
Revamping hardware persistency models: view-based and axiomatic persistency models for Intel-x86 and Armv8
inferred← citeshttps://doi.org/10.1145/3453483.3454081openalex-snapshot
Automatically enforcing fresh and consistent inputs in intermittent systems
inferred← citeshttps://doi.org/10.1145/3453483.3454105openalex-snapshot
Mirror: making lock-free data structures persistent
inferred← citeshttps://doi.org/10.1145/3458926openalex-snapshot
Armed Cats
inferred← citeshttps://doi.org/10.1145/3465402openalex-snapshot
Persistent Memory
inferred← citeshttps://doi.org/10.1145/3477132.3483556openalex-snapshot
Witcher
inferred← citeshttps://doi.org/10.1145/3477132.3483579openalex-snapshot
J-NVM
inferred← citeshttps://doi.org/10.1145/3498683openalex-snapshot
Extending Intel-x86 consistency and persistency: formalising the semantics of Intel-x86 memory types and non-temporal stores
inferred← citeshttps://doi.org/10.1145/3503221.3508436openalex-snapshot
FliT
inferred← citeshttps://doi.org/10.1145/3571219openalex-snapshot
The Path to Durable Linearizability
inferred← citeshttps://doi.org/10.1145/3571253openalex-snapshot
Taking Back Control in an Intermediate Representation for GPU Computing
inferred← citeshttps://doi.org/10.1145/3591250openalex-snapshot
A Type System for Safe Intermittent Computing
inferred← citeshttps://doi.org/10.1145/3620665.3640407openalex-snapshot
Skip It: Take Control of Your Cache!
inferred← citeshttps://doi.org/10.1145/3622820openalex-snapshot
Spirea: A Mechanized Concurrent Separation Logic for Weak Persistent Memory
inferred← citeshttps://doi.org/10.1145/3639476openalex-snapshot
Proceedings of the 2024 ACM/IEEE 44th International Conference on Software Engineering: New Ideas and Emerging Results
inferred← citeshttps://doi.org/10.1145/3669940.3707269openalex-snapshot
Robustness Verification for Checking Crash Consistency of Non-volatile Memory
inferred← citeshttps://doi.org/10.1145/3689781openalex-snapshot
Semantics of Remote Direct Memory Access: Operational and Declarative Models of RDMA on TSO Architectures
inferred← citeshttps://doi.org/10.1145/3689792openalex-snapshot
Compositionality and Observational Refinement for Linearizability with Crashes
inferred← citeshttps://doi.org/10.1145/3716311openalex-snapshot
Modal Crash Types for WAR-Aware Intermittent Computing
inferred← citeshttps://doi.org/10.1145/3763100openalex-snapshot
Shaking Up Quantum Simulators with Fuzzing and Rigour
inferred← citeshttps://doi.org/10.46298/lmcs-18(3:7)2022openalex-snapshot
Modularising Verification Of Durable Opacity
inferred← citeshttps://doi.org/10.48550/arxiv.2010.13593openalex-snapshot
Taming x86-TSO Persistency (Extended Version)
inferred← citeshttps://doi.org/10.48550/arxiv.2108.04202openalex-snapshot
FliT: A Library for Simple and Efficient Persistent Algorithms
Editorial review for independent work. ICSAC — the Institute for Complexity Science and Advanced Computing — runs a structured editorial panel for researchers publishing outside journals, and publishes on CiteStamp rails. Submission is free and goes through ORCID: icsacinstitute.org/submit.