Neil Davies
Research Subjects
Neil Davies has a total of 35 co-authors. Here are the top co-authors by number of shared publications:
- Peter Thompson
Predictable Network Solutions Ltd. (PNSol), Stonehouse GL10 2PG, UK
4 shared publications James Chapman
2 shared publications- James Chapman
IOHK
2 shared publications Kevin Hammond
2 shared publications- Kevin Hammond
University of St Andrews
2 shared publications Peter Van Roy
2 shared publications
Latest Publications
- Open Access
- 13 September 2025
- Published by Elsevier in Journal of Logical and Algebraic Methods in Programming
- Vol. 148
Algebraic reasoning for timeliness-guided system design
- 13 September 2025
- Published by Elsevier in Journal of Logical and Algebraic Methods in Programming
- Vol. 148
Open AccessAlgebraic reasoning for timeliness-guided system design
- Open Access
A Lower Bound on Latency Spikes for Capacity-Seeking Network Traffic
Most Internet traffic is carried by capacity-seeking protocols such as TCP and QUIC. Capacity-seeking protocols probe to find the maximum available throughput from sender to receiver, and, once they converge, attempt to keep sending traffic at this maximum rate. Achieving reliable low latency with capacity-seeking end-to-end methods is not yet entirely solved. We contribute a theoretical analysis to this ongoing discussion. In this work, we derive an expression for the minimum size of the spike in latency caused by a sudden drop in network capacity. Our results highlight a quantifiable and fundamental constraint on capacity-seeking network traffic. When end-to-end capacity is suddenly reduced, capacity-seeking traffic inevitably produces a latency spike. A lower bound on this latency spike can be calculated by multiplying the round-trip delay from the network bottleneck to the source of capacity-seeking traffic by the magnitude of the end-to-end capacity reduction. Testbed experiments show that this bound holds for the DCTCP, BBR, and Cubic congestion control algorithms. Our results have implications for the design of low-latency PHY and MAC-layer technologies because we quantify an important transport-layer consequence of unstable traffic rates.
Open AccessA Lower Bound on Latency Spikes for Capacity-Seeking Network Traffic
Most Internet traffic is carried by capacity-seeking protocols such as TCP and QUIC. Capacity-seeking protocols probe to find the maximum available throughput from sender to receiver, and, once they converge, attempt to keep sending traffic at this maximum rate. Achieving reliable low latency with capacity-seeking end-to-end methods is not yet entirely solved. We contribute a theoretical analysis to this ongoing discussion. In this work, we derive an expression for the minimum size of the spike in latency caused by a sudden drop in network capacity. Our results highlight a quantifiable and fundamental constraint on capacity-seeking network traffic. When end-to-end capacity is suddenly reduced, capacity-seeking traffic inevitably produces a latency spike. A lower bound on this latency spike can be calculated by multiplying the round-trip delay from the network bottleneck to the source of capacity-seeking traffic by the magnitude of the end-to-end capacity reduction. Testbed experiments show that this bound holds for the DCTCP, BBR, and Cubic congestion control algorithms. Our results have implications for the design of low-latency PHY and MAC-layer technologies because we quantify an important transport-layer consequence of unstable traffic rates.
- Open Access
Mind Your Outcomes: The ΔQSD Paradigm for Quality-Centric Systems Development and Its Application to a Blockchain Case Study
This paper directly addresses a long-standing issue that affects the development of many complex distributed software systems: how to establish quickly, cheaply, and reliably whether they can deliver their intended performance before expending significant time, effort, and money on detailed design and implementation. We describe SD, a novel metrics-based and quality-centric paradigm that uses formalised outcome diagrams to explore the performance consequences of design decisions, as a performance blueprint of the system. The distinctive feature of outcome diagrams is that they capture the essential observational properties of the system, independent of the details of system structure and behaviour. The SD paradigm derives bounds on performance expressed as probability distributions encompassing all possible executions of the system. The SD paradigm is both effective and generic: it allows values from various sources to be combined in a rigorous way so that approximate results can be obtained quickly and subsequently refined. SD has been successfully used by a small team in Predictable Network Solutions for consultancy on large-scale applications in a number of industries, including telecommunications, avionics, and space and defence, resulting in cumulative savings worth billions of US dollars. The paper outlines the SD paradigm, describes its formal underpinnings, and illustrates its use via a topical real-world example taken from the blockchain/cryptocurrency domain. SD has supported the development of an industry-leading proof-of-stake blockchain implementation that reliably and consistently delivers blocks of up to 80 kB every 20 s on average across a globally distributed network of collaborating block-producing nodes operating on the public internet.Open AccessMind Your Outcomes: The ΔQSD Paradigm for Quality-Centric Systems Development and Its Application to a Blockchain Case Study
This paper directly addresses a long-standing issue that affects the development of many complex distributed software systems: how to establish quickly, cheaply, and reliably whether they can deliver their intended performance before expending significant time, effort, and money on detailed design and implementation. We describe SD, a novel metrics-based and quality-centric paradigm that uses formalised outcome diagrams to explore the performance consequences of design decisions, as a performance blueprint of the system. The distinctive feature of outcome diagrams is that they capture the essential observational properties of the system, independent of the details of system structure and behaviour. The SD paradigm derives bounds on performance expressed as probability distributions encompassing all possible executions of the system. The SD paradigm is both effective and generic: it allows values from various sources to be combined in a rigorous way so that approximate results can be obtained quickly and subsequently refined. SD has been successfully used by a small team in Predictable Network Solutions for consultancy on large-scale applications in a number of industries, including telecommunications, avionics, and space and defence, resulting in cumulative savings worth billions of US dollars. The paper outlines the SD paradigm, describes its formal underpinnings, and illustrates its use via a topical real-world example taken from the blockchain/cryptocurrency domain. SD has supported the development of an industry-leading proof-of-stake blockchain implementation that reliably and consistently delivers blocks of up to 80 kB every 20 s on average across a globally distributed network of collaborating block-producing nodes operating on the public internet. - Open Access
- 24 January 2022
- Published by MDPI AG in Preprints.org
Mind Your Outcomes: The ∆Q approach to Quality-Centric Systems Development and Its Application to a Blockchain Case-Study
This paper directly addresses a long-standing issue that affects the development of many complex distributed software systems: how to establish quickly, cheaply, and reliably whether they can deliver their intended performance before expending significant time, effort and money on detailed design and implementation. We describe ∆QSD, a novel metrics-based and quality-centric paradigm that uses formalised outcome diagrams to explore the performance consequences of design decisions, as a performance blueprint of the system. The distinctive feature of outcome diagrams is that they capture the essential observational properties of the system, independent of the details of system structure and behaviour. The ∆QSD paradigm derives bounds on performance expressed as probability distributions encompassing all possible executions of the system. The ∆QSD paradigm is both effective and generic: it allows values from various sources to be combined in a rigorous way, so that approximate results can be obtained quickly and subsequently refined. ∆QSD has been successfully used by Predictable Network Solutions for consultancy on large-scale applications in a number of industries, including telecommunications, avionics, and space and defence, resulting in cumulative savings worth billions of US dollars. The paper outlines the ∆QSD paradigm, describes its formal underpinnings, and illustrates its use via a topical real-world example taken from the blockchain/cryptocurrency domain. ∆QSD has enabled challenging throughput targets to be met for a globally distributed blockchain operating on the public internet.
- 24 January 2022
- Published by MDPI AG in Preprints.org
Open AccessMind Your Outcomes: The ∆Q approach to Quality-Centric Systems Development and Its Application to a Blockchain Case-Study
This paper directly addresses a long-standing issue that affects the development of many complex distributed software systems: how to establish quickly, cheaply, and reliably whether they can deliver their intended performance before expending significant time, effort and money on detailed design and implementation. We describe ∆QSD, a novel metrics-based and quality-centric paradigm that uses formalised outcome diagrams to explore the performance consequences of design decisions, as a performance blueprint of the system. The distinctive feature of outcome diagrams is that they capture the essential observational properties of the system, independent of the details of system structure and behaviour. The ∆QSD paradigm derives bounds on performance expressed as probability distributions encompassing all possible executions of the system. The ∆QSD paradigm is both effective and generic: it allows values from various sources to be combined in a rigorous way, so that approximate results can be obtained quickly and subsequently refined. ∆QSD has been successfully used by Predictable Network Solutions for consultancy on large-scale applications in a number of industries, including telecommunications, avionics, and space and defence, resulting in cumulative savings worth billions of US dollars. The paper outlines the ∆QSD paradigm, describes its formal underpinnings, and illustrates its use via a topical real-world example taken from the blockchain/cryptocurrency domain. ∆QSD has enabled challenging throughput targets to be met for a globally distributed blockchain operating on the public internet.
- Open Access
- 18 August 2020
- Published by Springer Nature
- p. 94-120
Flexible Formality Practical Experience with Agile Formal Methods
- 18 August 2020
- Published by Springer Nature
- p. 94-120
Open AccessFlexible Formality Practical Experience with Agile Formal Methods
- Open Access
Towards a RINA-Based Architecture for Performance Management of Large-Scale Distributed Systems
Modern society is increasingly dependent on reliable performance of distributed systems. In this paper, we provide a precise definition of performance using the concept of quality attenuation; discuss its properties, measurement and decomposition; identify sources of such attenuation; outline methods of managing performance hazards automatically using the capabilities of the Recursive InterNetworking Architecture (RINA); demonstrate procedures for aggregating both application demands and network performance to achieve scalability; discuss dealing with bursty and time-critical traffic; propose metrics to assess the effectiveness of a performance management system; and outline an architecture for performance management.
Open AccessTowards a RINA-Based Architecture for Performance Management of Large-Scale Distributed Systems
Modern society is increasingly dependent on reliable performance of distributed systems. In this paper, we provide a precise definition of performance using the concept of quality attenuation; discuss its properties, measurement and decomposition; identify sources of such attenuation; outline methods of managing performance hazards automatically using the capabilities of the Recursive InterNetworking Architecture (RINA); demonstrate procedures for aggregating both application demands and network performance to achieve scalability; discuss dealing with bursty and time-critical traffic; propose metrics to assess the effectiveness of a performance management system; and outline an architecture for performance management.
- 1 February 2020
- Published by Institute of Electrical and Electronics Engineers (IEEE)
- p. 29-34
Towards a performance management architecture for large-scale distributed systems using RINA
Performance management of distributed systems is becoming increasingly important for the smooth functioning of society. In this paper we provide a precise definition of performance using the concept of quality attenuation, identify sources of such attenuation, outline methods of managing them automatically using the capabilities of the Recursive InterNetworking Architecture (RINA), and propose metrics to assess the effectiveness of a performance management system.
- 1 February 2020
- Published by Institute of Electrical and Electronics Engineers (IEEE)
- p. 29-34
Towards a performance management architecture for large-scale distributed systems using RINA
Performance management of distributed systems is becoming increasingly important for the smooth functioning of society. In this paper we provide a precise definition of performance using the concept of quality attenuation, identify sources of such attenuation, outline methods of managing them automatically using the capabilities of the Recursive InterNetworking Architecture (RINA), and propose metrics to assess the effectiveness of a performance management system.
- Open Access
- 1 November 2018
- Published by Oxford University Press (OUP) in European Journal of Public Health
- Vol. 28 (suppl_4)
Assessing the impact of PD-1/PD-L1 inhibitors on health and budget in Belgium
Background:
- 1 November 2018
- Published by Oxford University Press (OUP) in European Journal of Public Health
- Vol. 28 (suppl_4)
Open AccessAssessing the impact of PD-1/PD-L1 inhibitors on health and budget in Belgium
Background: