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.
1 January 2013 in Lecture Notes in Computer Science
Implementing Programming Languages (PLs) has always been a challenge for various reasons. One reason is the excess of routine tasks to be redone on every implementation cycle. This is despite the remarkable fraction of syntax and semantics usually shared between successive cycles. In this paper, we present a component-based approach to avoid reimplementation of shared PL fractions. We provide two sets of reusable components; one for syntax implementation and another for semantics. Our syntax and semantics components correspond to syntactic categories and semantics rules of a PL specification, respectively. We show how, in addition to their service to reusability in syntax and semantics, our components can cater reusable implementation of PL analyses. Our current level of experimentation suggests that this approach is applicable wherever the following two features are available or can be simulated: Type Constraints and Multiple Inheritance. Implementing a PL using our approach, however, requires some modest programming discipline that we will explain throughout the text.
We present a work in progress report on a new programming model that supports declarative, functional style aggregation operations over devices at the edge. This programming model bridges the gap between the two competing approaches for large-scale aggregations, streaming all data back to a central coordinator versus designing an optimized, distributed algorithm, by leveraging convergent data structures, dynamic scoping, and a declarative functional semantics implemented by a distributed runtime. We motivate our design with an industrial application susceptible to message reordering and arbitrary message delays on an unreliable network.
Template and Preprocessor Metaprogramming are both well-known in the C++ community to have much in common with Functional Programming (FP). Recently, very few research threads on underpinning these commonalities have emerged to empower cross-development of C++ Metaprogramming (C++MP) and FP. In this paper, we program a self-contained real-world example in a side-by-side fashion to explore the usefulness of a few mainstream FP languages for this purpose: We develop a compile-time abstract datatype for Rational Numbers in C++. We then present the runtime equivalent in HASKELL, F#, and Scala to discuss some FP parallels across the languages. Here, we consider semi-automatic translation between C++MP and FP languages, for earlier studies on these parallels have already obviated the impracticability of fully automatic translations. Our study also shows the superiority of multiparadigm FP languages over single-paradigm ones. In particular, we conclude Scala to currently be the most promising FP language for facilitating C++MP.
10 August 2016 in Electronic Proceedings in Theoretical Computer Science
Interactions between internet users are mediated by their devices and the common support infrastructure in data centres. Keeping track of causality amongst actions that take place in this distributed system is key to provide a seamless interaction where effects follow causes. Tracking causality in large scale interactions is difficult due to the cost of keeping large quantities of metadata; even more challenging when dealing with resource-limited devices. In this paper, we focus on keeping partial knowledge on causality and address deduction from that knowledge. We provide the first proof-theoretic causality modelling for distributed partial knowledge. We prove computability and consistency results. We also prove that the partial knowledge gives rise to a weaker model than classical causality. We provide rules for offline deduction about causality and refute some related folklore. We define two notions of forward and backward bisimilarity between devices, using which we prove two important results. Namely, no matter the order of addition/removal, two devices deduce similarly about causality so long as: (1) the same causal information is fed to both. (2) they start bisimilar and erase the same causal information. Thanks to our establishment of forward and backward bisimilarity, respectively, proofs of the latter two results work by simple induction on length.Comment: In Proceedings ICE 2016, arXiv:1608.0313