Abstract

Abstract
We present Caos: a programming framework for computer-aided design of structural operational semantics for formal models. This framework includes a set of Scala libraries and a workflow to produce visual and interactive diagrams that animate and provide insights over the structure and the semantics of a given abstract model with operational rules. Caos follows an approach where theoretical foundations and a practical tool are built together, as an alternative to foundations-first design (tool justifies theory) or tool-first design (foundations justify practice). The advantage of Caos is that the tool-under-development can immediately be used to automatically run numerous and sizeable examples in order to identify subtle mistakes, unexpected outcomes, and unforeseen limitations in the foundations-under-development, as early as possible. More concretely, Caos supports the quick creation of interactive websites that help the end-users better understand a new language, structure, or analysis. End-users can be research colleagues trying to understand a companion paper or students learning about a new simple language or operational semantics. We include a list of open-source projects with a web frontend supported by Caos that are used both in research and teaching contexts.

Abstract

Abstract
The growth in cloud computing, Big Data, AI and high-performance computing (HPC) necessitate the deployment of additional data centers (DC's) with high energy demands. The unprecedented increase in the Thermal Design Power (TDP) of the computing chips will require innovative cooling techniques. Furthermore, DC's are increasingly limited in their ability to add powerful GPU servers by power capacity constraints. As cooling energy use accounts for up to 40% of DC energy consumption, creative cooling solutions are urgently needed to allow deployment of additional servers, enhance sustainability and increase energy efficiency of DC's. The information in this study is provided from Start Campus' Sines facility supported by Alfa Laval for the heat exchanger and CO2 emission calculations. The study evaluates the performance and sustainability impact of various data center cooling strategies including an air-only deployment and a subsequent hybrid air/water cooling solution all utilizing sea water as the cooling source. We evaluate scenarios from 3 MW to 15+1 MW of IT load in 3 MW increments which correspond to the size of heat exchangers used in the Start Campus' modular system design. This study also evaluates the CO2 emissions compared to a conventional chiller system for all the presented scenarios. Results indicate that the effective use of the sea water cooled system combined with liquid cooled systems improve the efficiency of the DC, plays a role in decreasing the CO2 emissions and supports in achieving sustainability goals.

Abstract
We present an adequacy theorem for a concurrent extension of probabilistic GCL. The underlying denotational semantics is based on the so-called mixed powerdomains, which combine non-determinism with probabilistic behaviour. The theorem itself is formulated via M. Smyth's idea of treating observable properties as open sets of a topological space. The proof hinges on a 'topological generalisation' of Konig's lemma in the setting of probabilistic programming (a result that is proved in the paper as well). One application of the theorem is that it entails semi-decidability w.r.t. whether a concurrent program satisfies an observable property (written in a certain form). This is related to M. Escardo's conjecture about semi-decidability w.r.t. may and must probabilistic testing.

Abstract
Data loaders are used by Machine Learning (ML) frameworks like PyTorch and TensorFlow to apply transformations to data before feeding it into the accelerator. This operation is called data preprocessing. Data preprocessing plays an important role in the ML training workflow because if it is inefficiently pipelined with the training, it can yield high GPU idleness, resulting in important training delays. Unfortunately, existing data loaders turn out to waste GPU resources, with $76\%$ GPU idleness when using the PyTorch data loader, for example. One key source of inefficiency is the variability in preprocessing time across samples within the same dataset. Existing data loaders are oblivious to this variability, and they construct batches without any consideration of slow or fast samples. In this case, the entire batch is delayed by a single slow sample, stalling the training pipeline and resulting in head-of-line blocking. To address these inefficiencies, we present MinatoLoader, a general-purpose data loader for PyTorch that accelerates training and improves GPU utilization. MinatoLoader is designed for a single-server setup, containing multiple GPUs. It continuously prepares data in the background and actively constructs batches by prioritizing fast-to-preprocess samples, while slower samples are processed in parallel. We evaluate MinatoLoader on servers with V100 and A100 GPUs. On a machine with four A100 GPUs, MinatoLoader improves the training time of a wide range of workloads by up to $7.5\times$ ($3.6\times$ on average) over PyTorch DataLoader and Pecan, and up to $3\times$ ($2.2\times$ on average) over DALI. It also increases average GPU utilization from 46.4\% with PyTorch to 90.45\%, while preserving model accuracy and enabling faster convergence.