arXiv subjects

Blair Archibald

Publications and source records attributed to Blair Archibald.

12 recordsLinked to original sources

arXiv2025

Signalling Health for Improved Kubernetes Microservice Availability

Microservices are often deployed and managed by a container orchestrator that can detect and fix failures to maintain the service availability critical in many applications. In Poll-based Container Monitoring (PCM), the orchestrator periodically checks container health. While a common approach, PCM requires careful tuning, may degrade service availability, and can be slow to detect container health changes. An alternative is Signal-based Container Monitoring (SCM), where the container signals the orchestrator when its status changes. We present the design, implementation, and evaluation of an SCM approach for Kubernetes and empirically show that it has benefits over PCM, as predicted by a new mathematical model. We compare the service availability of SCM and PCM over six experiments using the SockShop benchmark. SCM does not require that polling intervals are tuned, and yet detects container failure 86\% faster than PCM and container readiness in a comparable time with limited resource overheads. We find PCM can erroneously detect failures, and this reduces service availability by 4\%. We propose that orchestrators offer SCM features for faster failure detection than PCM without erroneous detections or careful tuning.

cs.DC↗

arXiv2025

A Digital Twinning Approach to Decarbonisation: Research Challenges

Transportation accounts for around 27% of green house gas emissions in the UK. While an obvious priority area for decarbonisation, and aligned to the UK government goal of reducing emissions by 68% for 2030, the free-market nature of the transportation sector combined with its fundamentally implicit and pervasive connections to all aspects of society and national infrastructure mean that all decarbonisation efforts to date have been siloed within a single transport sector, e.g. only considering greener aviation fuels. Truly decarbonising transport requires radical changes to the entire transport infrastructure, and since that transport does not happen in isolation, a single user often using multiple modes, we need a view over the whole transport system. The first step to solving a problem is to understand it. As a result of the fragmented nature of the transportation sector, there is currently no system level view. Without the ability to monitor even adjacent transport domains, the ability for people or organisations to (dynamically) adapt their operations for decarbonisation outcomes is unrealistic. As transportation is a complex social-techno-economic system, information and knowledge sharing is a must to be able to understand and explore potential solutions to the decarbonisation challenge. We believe a Federated Digital Twinning Approach has the potential to tackle transport decarbonisation problems, and, in this extended abstract, we give an overview of the research required to tackle the fundamental challenges around digital twin design, generation, validation and verification.

eess.SY↗

arXiv2025

Modelling Real-time Systems with Bigraphs

Bigraphical Reactive Systems (BRSs) are a graph-rewriting formalism describing systems evolving in two dimensions: spatially, e.g. a person in a room, and non-spatially, e.g. mobile phones communicating regardless of location. Despite use in domains including communication protocols, agent programming, biology, and security, there is no support for real-time systems. We extend BRSs to support real-time systems with a modelling approach that uses multiple perspectives to represent digital clocks. We use Action BRSs, a recent extension of BRSs, where the resulting transition system is a Markov Decision Process (MDP). This allows a natural representation of the choices in each system state: to either allow time to pass or perform a specific action. We implement our proposed approach using the BigraphER toolkit, and demonstrate the effectiveness through multiple examples including modelling cloud system requests.

cs.LO↗

arXiv2024

Practical Modelling with Bigraphs

Bigraphs are a versatile modelling formalism that allows easy expression of placement and connectivity relations in a graphical format. System evolution is user defined as a set of rewrite rules. This paper presents a practical, yet detailed guide to developing, executing, and reasoning about bigraph models, including recent extensions such as parameterised, instantaneous, prioritised and conditional rules, and probabilistic and stochastic rewriting.

cs.LO↗

arXiv2024

The Effect of Predictive Formal Modelling at Runtime on Performance in Human-Swarm Interaction

Formal Modelling is often used as part of the design and testing process of software development to ensure that components operate within suitable bounds even in unexpected circumstances. In this paper, we use predictive formal modelling (PFM) at runtime in a human-swarm mission and show that this integration can be used to improve the performance of human-swarm teams. We recruited 60 participants to operate a simulated aerial swarm to deliver parcels to target locations. In the PFM condition, operators were informed of the estimated completion times given the number of drones deployed, whereas in the No-PFM condition, operators did not have this information. The operators could control the mission by adding or removing drones from the mission and thereby, increasing or decreasing the overall mission cost. The evaluation of human-swarm performance relied on four key metrics: the time taken to complete tasks, the number of agents involved, the total number of tasks accomplished, and the overall cost associated with the human-swarm task. Our results show that PFM modelling at runtime improves mission performance without significantly affecting the operator's workload or the system's usability.

cs.RO↗

arXiv2022

Parallel Flowshop in YewPar

Parallelism may reduce the time to find exact solutions for many Operations Research (OR) problems, but parallelising combinatorial search is extremely challenging. YewPar is a new combinatorial search framework designed to allow domain specialists to benefit from parallelism by reusing sophisticated parallel search patterns. This paper shows (1) that it is low effort to encode and parallelise a typical OR problem (Flowshop Scheduling FSP) in YewPar even for scalable clusters; (2) that the YewPar library makes it extremely easy to exploit three alternate FSP parallelisations; (3) that the YewPar FSP implementations are valid, and have sequential performance comparable with a published algorithm; and (4) provides a systematic performance evaluation of the three parallel FSP versions on 10 standard FSP instances with up to 240 workers on a Beowulf cluster.

cs.DC↗

arXiv2022

FAIR Data Pipeline: provenance-driven data management for traceable scientific workflows

Modern epidemiological analyses to understand and combat the spread of disease depend critically on access to, and use of, data. Rapidly evolving data, such as data streams changing during a disease outbreak, are particularly challenging. Data management is further complicated by data being imprecisely identified when used. Public trust in policy decisions resulting from such analyses is easily damaged and is often low, with cynicism arising where claims of "following the science" are made without accompanying evidence. Tracing the provenance of such decisions back through open software to primary data would clarify this evidence, enhancing the transparency of the decision-making process. Here, we demonstrate a Findable, Accessible, Interoperable and Reusable (FAIR) data pipeline developed during the COVID-19 pandemic that allows easy annotation of data as they are consumed by analyses, while tracing the provenance of scientific outputs back through the analytical source code to data sources. Such a tool provides a mechanism for the public, and fellow scientists, to better assess the trust that should be placed in scientific evidence, while allowing scientists to support policy-makers in openly justifying their decisions. We believe that tools such as this should be promoted for use across all areas of policy-facing research.

q-bio.QM↗

arXiv2021

Observable and Attention-Directing BDI Agents for Human-Autonomy Teaming

Human-autonomy teaming (HAT) scenarios feature humans and autonomous agents collaborating to meet a shared goal. For effective collaboration, the agents must be transparent and able to share important information about their operation with human teammates. We address the challenge of transparency for Belief-Desire-Intention agents defined in the Conceptual Agent Notation (CAN) language. We extend the semantics to model agents that are observable (i.e. the internal state of tasks is available), and attention-directing (i.e. specific states can be flagged to users), and provide an executable semantics via an encoding in Milner's bigraphs. Using an example of unmanned aerial vehicles, the BigraphER tool, and PRISM, we show and verify how the extensions work in practice.

cs.MA↗

arXiv2021

Modelling and Verifying BDI Agents with Bigraphs

The Belief-Desire-Intention (BDI) architecture is a popular framework for rational agents; most verification approaches are based on reasoning about implementations of BDI programming languages. We investigate an alternative approach based on reasoning about BDI agent semantics, through a model of the execution of an agent program. We employ Milner's bigraphs as the modelling framework and present an encoding for the Conceptual Agent Notation (CAN) language - a superset of AgentSpeak featuring declarative goals, concurrency, and failure recovery. We provide an encoding of the syntax and semantics of CAN agents, and give a rigorous proof that the encoding is faithful. Verification is based on the use of mainstream software tools including BigraphER, and a small case study verifying several properties of Unmanned Aerial Vehicles (UAVs) illustrates the framework in action. The executable framework is a foundational step that will enable more advanced reasoning such as plan preference, intention priorities and trade-offs, and interactions with an environment under uncertainty.

cs.PL↗

arXiv2021

Probablistic Bigraphs

Bigraphs are a universal computational modelling formalism for the spatial and temporal evolution of a system in which entities can be added and removed. We extend bigraphs to probablistic bigraphs, and then again to action bigraphs, which include non-determinism and rewards. The extensions are implemented in the BigraphER toolkit and illustrated through examples of virus spread in computer networks and data harvesting in wireless sensor systems. BigraphER also supports the existing stochastic bigraphs extension of Krivine et al., and using BigraphER we give, for the first time, a direct implementation of the membrane budding model used to motivate stochastic bigraphs.

cs.LO↗

arXiv2018

Functional Baby Talk: Analysis of Code Fragments from Novice Haskell Programmers

What kinds of mistakes are made by novice Haskell developers, as they learn about functional programming? Is it possible to analyze these errors in order to improve the pedagogy of Haskell? In 2016, we delivered a massive open online course which featured an interactive code evaluation environment. We captured and analyzed 161K interactions from learners. We report typical novice developer behavior; for instance, the mean time spent on an interactive tutorial is around eight minutes. Although our environment was restricted, we gain some understanding of Haskell novice errors. Parenthesis mismatches, lexical scoping errors and do block misunderstandings are common. Finally, we make recommendations about how such beginner code evaluation environments might be enhanced.

cs.PL↗

arXiv2017

Replicable Parallel Branch and Bound Search

Combinatorial branch and bound searches are a common technique for solving global optimisation and decision problems. Their performance often depends on good search order heuristics, refined over decades of algorithms research. Parallel search necessarily deviates from the sequential search order, sometimes dramatically and unpredictably, e.g. by distributing work at random. This can disrupt effective search order heuristics and lead to unexpected and highly variable parallel performance. The variability makes it hard to reason about the parallel performance of combinatorial searches. This paper presents a generic parallel branch and bound skeleton, implemented in Haskell, with replicable parallel performance. The skeleton aims to preserve the search order heuristic by distributing work in an ordered fashion, closely following the sequential search order. We demonstrate the generality of the approach by applying the skeleton to 40 instances of three combinatorial problems: Maximum Clique, 0/1 Knapsack and Travelling Salesperson. The overheads of our Haskell skeleton are reasonable: giving slowdown factors of between 1.9 and 6.2 compared with a class-leading, dedicated, and highly optimised C++ Maximum Clique solver. We demonstrate scaling up to 200 cores of a Beowulf cluster, achieving speedups of 100x for several Maximum Clique instances. We demonstrate low variance of parallel performance across all instances of the three combinatorial problems and at all scales up to 200 cores, with median Relative Standard Deviation (RSD) below 2%. Parallel solvers that do not follow the sequential search order exhibit far higher variance, with median RSD exceeding 85% for Knapsack.

cs.DC↗