Abstract
The algebra of programming (AoP) is a discipline for programming from specifications using relation algebra. Specification vagueness and nondeterminism are captured by relations. (Final) implementations are functions. Probabilistic functions are half way between relations and functions: they express the propensity, or likelihood of ambiguous, multiple outputs. This paper puts forward a basis for a linear algebra of programming (LAoP) extending standard AoP towards probabilistic functions. Because of the quantitative essence of these functions, the allegory of binary relations which supports the AoP has to be extended. We show that, if one restricts to discrete probability spaces, categories of matrices provide adequate support for the extension, while preserving the pointfree reasoning style typical of the AoP.

Abstract
There is a need for a language able to reconcile the recent upsurge of interest in quantitative methods in the software sciences with logic and set theory that have been used for so many years in capturing the qualitative aspects of the same body of knowledge. Such a lingua franca should be typed, polymorphic, diagrammatic, calculational and easy to blend with traditional notation. This paper puts forward typed linear algebra (LA) as a candidate notation for such a role. Typed LA emerges from regarding matrices as morphisms of suitable categories whereby traditional linear algebra is equipped with a type system. In this paper we show typed LA at work in describing weighted (probabilistic) automata. Some attention is paid to the interface between the index-free language of matrix combinators and the corresponding index-wise notation, so as to blend with traditional set theoretic notation. © 2012 Springer-Verlag.

Abstract
In a recent article [1], David Parnas questions the traditional use of formal methods in software development, which he considers an underdeveloped body of knowledge and therefore of little hope for the software industry. He confronts the reader with the following statement, at some stage: "We must learn to use mathematics in software development, but we need to question, and be prepared to discard, most of the methods that we have been discussing and promoting for all these years." At the core of Parnas objections we find the contrast between the current ad-hoc (re)invention of mathematical concepts which are cumbersome and a burden to use and elegant (and therefore useful) concepts which are neglected, often for cultural or (lack of) background reasons. © 2012 Springer-Verlag.

Abstract

Abstract
Gossip, or epidemic, protocols have emerged as a highly scalable and resilient approach to implement several application level services such as reliable multicast, data aggregation, publish-subscribe, among others. All these protocols organize nodes in an unstructured random overlay network. In many cases, it is interesting to bias the random overlay in order to optimize some efficiency criteria, for instance, to reduce the stretch of the overlay routing. In this paper, we propose X-BOT, a new protocol that allows to bias the topology of an unstructured gossip overlay network. X-BOT is completely decentralized and, unlike previous approaches, preserves several key properties of the original (nonbiased) overlay (most notably, the node degree and consequently, the overlay connectivity). Experimental results show that X-BOT can generate more efficient overlays than previous approaches independently of the underlying physical network topology.

Abstract
Deduplication is widely accepted as an effective technique for eliminating duplicated data in backup and archival systems. Nowadays, deduplication is also becoming appealing in cloud computing, where large-scale virtualized storage infrastructures hold huge data volumes with a significant share of duplicated content. There have thus been several proposals for embedding deduplication in storage appliances and file systems, providing different performance trade-offs while targeting both user and application data, as well as virtual machine images. It is however hard to determine to what extent is deduplication useful in a particular setting and what technique will provide the best results. In fact, existing disk I/O micro-benchmarks are not designed for evaluating deduplication systems, following simplistic approaches for generating data written that lead to unrealistic amounts of duplicates. We address this with DEDISbench, a novel micro-benchmark for evaluating disk I/O performance of block based deduplication systems. As the main contribution, we introduce the generation of a realistic duplicate distribution based on real datasets. Moreover, DEDISbench also allows simulating access hotspots and different load intensities for I/O operations. The usefulness of DEDISbench is shown by comparing it with Bonnie++ and IOzone open-source disk I/O micro-benchmarks on assessing two open-source deduplication systems, Opendedup and Lessfs, using Ext4 as a baseline. As a secondary contribution, our results lead to novel insight on the performance of these file systems. © 2012 Springer-Verlag.