-
Algebraic Reasoning About Timeliness
Authors:
Seyed Hossein Haeri,
Peter W. Thompson,
Peter Van Roy,
Magne Haveraaen,
Neil J. Davies,
Mikhail Barash,
Kevin Hammond,
James Chapman
Abstract:
Designing distributed systems to have predictable performance under high load is difficult because of resource exhaustion, non-linearity, and stochastic behaviour. Timeliness, i.e., delivering results within defined time bounds, is a central aspect of predictable performance. In this paper, we focus on timeliness using the DELTA-Q Systems Development paradigm (DELTA-QSD, developed by PNSol), which…
▽ More
Designing distributed systems to have predictable performance under high load is difficult because of resource exhaustion, non-linearity, and stochastic behaviour. Timeliness, i.e., delivering results within defined time bounds, is a central aspect of predictable performance. In this paper, we focus on timeliness using the DELTA-Q Systems Development paradigm (DELTA-QSD, developed by PNSol), which computes timeliness by modelling systems observationally using so-called outcome expressions. An outcome expression is a compositional definition of a system's observed behaviour in terms of its basic operations. Given the behaviour of the basic operations, DELTA-QSD efficiently computes the stochastic behaviour of the whole system including its timeliness.
This paper formally proves useful algebraic properties of outcome expressions w.r.t. timeliness. We prove the different algebraic structures the set of outcome expressions form with the different DELTA-QSD operators and demonstrate why those operators do not form richer structures. We prove or disprove the set of all possible distributivity results on outcome expressions. On our way for disproving 8 of those distributivity results, we develop a technique called properisation, which gives rise to the first body of maths for improper random variables. Finally, we also prove 14 equivalences that have been used in the past in the practice of DELTA-QSD.
An immediate benefit is rewrite rules that can be used for design exploration under established timeliness equivalence. This work is part of an ongoing project to disseminate and build tool support for DELTA-QSD. The ability to rewrite outcome expressions is essential for efficient tool support.
△ Less
Submitted 21 August, 2023;
originally announced August 2023.
-
Ideas for the future of Prolog inspired by Oz
Authors:
Peter Van Roy,
Seif Haridi
Abstract:
Both Prolog and Oz are multiparadigm languages with a logic programming core. There is a significant subset of Oz that is a syntactic variant of Prolog: pure Prolog programs with green or blue cuts and bagof/3 or setof/3 can be translated directly to Oz. Because of this close relationship between Prolog and Oz, we propose that the extensions made by Oz to logic programming can be an inspiration fo…
▽ More
Both Prolog and Oz are multiparadigm languages with a logic programming core. There is a significant subset of Oz that is a syntactic variant of Prolog: pure Prolog programs with green or blue cuts and bagof/3 or setof/3 can be translated directly to Oz. Because of this close relationship between Prolog and Oz, we propose that the extensions made by Oz to logic programming can be an inspiration for the future evolution of Prolog. We explain three extensions, namely deterministic logic programming, lazy concurrent functional programming, and purely functional distributed computing. We briefly present these extensions and we explain how they can help Prolog evolve in its next 50 years.
△ Less
Submitted 1 February, 2023;
originally announced February 2023.
-
Proceedings of the 2nd Workshop on Logic and Practice of Programming (LPOP)
Authors:
David S. Warren,
Peter Van Roy,
Yanhong A. Liu
Abstract:
This proceedings contains abstracts and position papers for the work presented at the second Logic and Practice of Programming (LPOP) Workshop. The workshop was held online, virtually in place of Chicago, USA, on November 15, 2010, in conjunction with the ACM SIGPLAN Conference on Systems, Programming, Languages, and Applications: Software for Humanity (SPLASH) 2020. The purpose of this workshop i…
▽ More
This proceedings contains abstracts and position papers for the work presented at the second Logic and Practice of Programming (LPOP) Workshop. The workshop was held online, virtually in place of Chicago, USA, on November 15, 2010, in conjunction with the ACM SIGPLAN Conference on Systems, Programming, Languages, and Applications: Software for Humanity (SPLASH) 2020. The purpose of this workshop is to be a bridge between different areas of computer science that use logic as a practical tool. We take advantage of the common language of formal logic to exchange ideas between these different areas.
△ Less
Submitted 17 November, 2022;
originally announced November 2022.
-
LANSCE Digital Low Level RF Upgrade
Authors:
P. Van Rooy,
M. Prokop,
S. Kwon,
P. Torrez,
L. Castellano,
A. Archuleta,
C. Marchwinski
Abstract:
Incremental upgrades of the legacy low level RF (LLRF) equipment-50 years for the Los Alamos Neutron Science Center (LANSCE)-involves challenges and problems not seen with new and total replacement opportunities. The digital LLRF upgrade at LANSCE has deployed 30 of the 53 required systems as of September 2022. This paper describes the performance of the digital upgrade, current status, and future…
▽ More
Incremental upgrades of the legacy low level RF (LLRF) equipment-50 years for the Los Alamos Neutron Science Center (LANSCE)-involves challenges and problems not seen with new and total replacement opportunities. The digital LLRF upgrade at LANSCE has deployed 30 of the 53 required systems as of September 2022. This paper describes the performance of the digital upgrade, current status, and future installations along with the technical challenges, including unexpected challenges, associated with deploying new digital systems in conjunction with legacy analog equipment. In addition, this paper discusses the operational details of simultaneous multi-energy beam operations using high energy re-bunching, beam-type specific set points and simultaneous multi-beam operations at LANSCE. The adaptability of the digital LLRF systems is essential as the design is able to accommodate new control and beam parameters associated with future systems without significant hardware modifications such as the expected LANSCE Modernization Program. This adaptability of the digital LLRF technology was recently demonstrated with the Module 1, 201.25-MHz high-power RF upgrade completed in 2021.
△ Less
Submitted 27 October, 2022; v1 submitted 12 October, 2022;
originally announced October 2022.
-
Disturbance Observer Application for the Compensation of the Phase Drift of the LANSCE DTL LINAC Solid State Power Amplifier
Authors:
Sungil Kwon,
M. S. Barrueta,
L. Castellano,
J. M. Lyles,
M. Prokop,
P. Van Rooy,
P. Torrez
Abstract:
The front end of Los Alamos Neutron Science Center (LANSCE) linear accelerator uses four 201.25-MHz Drift-Tube Linacs (DTLs) to accelerate the H+ and H- beams to 100 MeV. Three of the 201.25-MHz DTLs are powered by diacrodes and the first DTL is powered by a tetrode. A 20-kW solid-state power amplifier (SSPA) is used to provide ~15 kW drive power to the tetrode. The SSPA is water-cooled and consis…
▽ More
The front end of Los Alamos Neutron Science Center (LANSCE) linear accelerator uses four 201.25-MHz Drift-Tube Linacs (DTLs) to accelerate the H+ and H- beams to 100 MeV. Three of the 201.25-MHz DTLs are powered by diacrodes and the first DTL is powered by a tetrode. A 20-kW solid-state power amplifier (SSPA) is used to provide ~15 kW drive power to the tetrode. The SSPA is water-cooled and consists of 24 push-pull LDMOS transistors operating at 45% of their power saturation capability, providing ample power headroom and excellent linearity. However, the phase of the SSPA is perturbed at +/-20 degrees over a few ten minutes partially caused by the temperature dependent phase variation of the air-cooled SSPA driver circulator. This phase variation consumes most of the phase control margin of the cavity field feedback controller. In order to mitigate the effect of the SSPA phase variation on the cavity field, a disturbance observer controller (DOBC) has been designed and implemented on the cavity field control FPGA, which functions in parallel with the cavity field feedback controller. In this paper, the DOBC design and its function as well as its short- and long-term performance are addressed.
△ Less
Submitted 14 November, 2022; v1 submitted 11 October, 2022;
originally announced October 2022.
-
MATLAB Scripts for RF Commissioning at the LANSCE LINAC
Authors:
Sungil Kwon,
A. Archuleta,
L. Castellano,
C. Marchwinski,
M. Prokop,
P. Van Rooy,
P. Torrez
Abstract:
The linear accelerator (LINAC) at the Los Alamos Neu-tron Science Center (LANSCE) consists of Pre-buncher, Main-Buncher, low-energy beam transport (LEBT), four 201.25-MHz Drift Tube Linacs (DTLs) and forty-four 805-MHz Coupled Cavity Linacs (CCLs). As a part of the upcoming LANSCE Modernization project, low-level RF (LLRF) systems of four 201-MHz DTLs and twenty-six 805-MHz SCLs have been digitize…
▽ More
The linear accelerator (LINAC) at the Los Alamos Neu-tron Science Center (LANSCE) consists of Pre-buncher, Main-Buncher, low-energy beam transport (LEBT), four 201.25-MHz Drift Tube Linacs (DTLs) and forty-four 805-MHz Coupled Cavity Linacs (CCLs). As a part of the upcoming LANSCE Modernization project, low-level RF (LLRF) systems of four 201-MHz DTLs and twenty-six 805-MHz SCLs have been digitized. Hence the net-work-based control of the cavity field and RF commis-sioning are possible. Each LLRF and high-power RF (HPRF) systems have many process variables (PVs) lo-cated on different computer control screens provided by the Extensible Display Manager (EDM). Several MATLAB m-scripts have been developed to efficiently process the necessary PVs while auto-start, ampli-tude/phase calibration, gain tuning of the cavity field feedback controllers, gain and phase tuning of the beam feedforward controllers, and high power RF trip recovery, processes are configured and validated. This paper ad-dresses the sequence of RF commissioning of the LANSCE LINAC from the time of RF-turn-on to beam feedforward control and its relevant EDMs and MATLAB m-scripts.
△ Less
Submitted 14 November, 2022; v1 submitted 11 October, 2022;
originally announced October 2022.
-
Latency-Sensitive Web Service Workflows: A Case for a Software-Defined Internet
Authors:
Pradeeban Kathiravelu,
Peter Van Roy,
Luís Veiga,
Elhadj Benkhelifa
Abstract:
The Internet, at large, remains under the control of service providers and autonomous systems. The Internet of Things (IoT) and edge computing provide an increasing demand and potential for more user control for their web service workflows. Network Softwarization revolutionizes the network landscape in various stages, from building, incrementally deploying, and maintaining the environment. Softwar…
▽ More
The Internet, at large, remains under the control of service providers and autonomous systems. The Internet of Things (IoT) and edge computing provide an increasing demand and potential for more user control for their web service workflows. Network Softwarization revolutionizes the network landscape in various stages, from building, incrementally deploying, and maintaining the environment. Software-Defined Networking (SDN) and Network Functions Virtualization (NFV) are two core tenets of network softwarization. SDN offers a logically centralized control plane by abstracting away the control of the network devices in the data plane. NFV virtualizes dedicated hardware middleboxes and deploys them on top of servers and data centers as network functions. Thus, network softwarization enables efficient management of the system by enhancing its control and improving the reusability of the network services. In this work, we propose our vision for a Software-Defined Internet (SDI) for latency-sensitive web service workflows. SDI extends network softwarization to the Internet-scale, to enable a latency-aware user workflow execution on the Internet.
△ Less
Submitted 14 May, 2020;
originally announced May 2020.
-
Achlys : Towards a framework for distributed storage and generic computing applications for wireless IoT edge networks with Lasp on GRiSP
Authors:
Kopestenski Igor,
Peter Van Roy
Abstract:
Internet of Things (IoT) has gained substantial attention over the past years. And the main discussion has been how to process the amount of data that it generates which has lead to the edge computing paradigm. Wether it is called fog1, edge or mist, the principle remains that cloud services must become available closer to clients. This documents presents ongoing work on future edge systems that a…
▽ More
Internet of Things (IoT) has gained substantial attention over the past years. And the main discussion has been how to process the amount of data that it generates which has lead to the edge computing paradigm. Wether it is called fog1, edge or mist, the principle remains that cloud services must become available closer to clients. This documents presents ongoing work on future edge systems that are built to provide steadfast IoT services to users by bringing storage and processing power closer to peripheral parts of networks. Designing such infrastructures is becoming much more challenging as the number of IoT devices keeps growing. Production grade deployments have to meet very high performance requirements, and end-to-end solutions involve significant investments. In this paper, we aim at providing a solution to extend the range of the edge model to the very farthest nodes in the network. Specifically, we focus on providing reliable storage and computation capabilities immediately on wireless IoT sensor nodes. This extended edge model will allow end users to manage their IoT ecosystem without forcibly relying on gateways or Internet provider solutions. In this document, we introduce Achlys, a prototype implementation of an edge node that is a concrete port of the Lasp programming library on the GRiSP Erlang embedded system. This way, we aim at addressing the need for a general purpose edge that is both resilient and consistent in terms of storage and network. Finally, we study example use cases that could take advantage of integrating the Achlys framework and discuss future work for the latter.
△ Less
Submitted 15 January, 2019;
originally announced January 2019.
-
On-Demand Big Data Integration: A Hybrid ETL Approach for Reproducible Scientific Research
Authors:
Pradeeban Kathiravelu,
Ashish Sharma,
Helena Galhardas,
Peter Van Roy,
Luıs Veiga
Abstract:
Scientific research requires access, analysis, and sharing of data that is distributed across various heterogeneous data sources at the scale of the Internet. An eager ETL process constructs an integrated data repository as its first step, integrating and loading data in its entirety from the data sources. The bootstrap** of this process is not efficient for scientific research that requires acc…
▽ More
Scientific research requires access, analysis, and sharing of data that is distributed across various heterogeneous data sources at the scale of the Internet. An eager ETL process constructs an integrated data repository as its first step, integrating and loading data in its entirety from the data sources. The bootstrap** of this process is not efficient for scientific research that requires access to data from very large and typically numerous distributed data sources. a lazy ETL process loads only the metadata, but still eagerly. Lazy ETL is faster in bootstrap**. However, queries on the integrated data repository of eager ETL perform faster, due to the availability of the entire data beforehand.
In this paper, we propose a novel ETL approach for scientific data integration, as a hybrid of eager and lazy ETL approaches, and applied both to data as well as metadata. This way, Hybrid ETL supports incremental integration and loading of metadata and data from the data sources. We incorporate a human-in-the-loop approach, to enhance the hybrid ETL, with selective data integration driven by the user queries and sharing of integrated data between users. We implement our hybrid ETL approach in a prototype platform, Obidos, and evaluate it in the context of data sharing for medical research. Obidos outperforms both the eager ETL and lazy ETL approaches, for scientific research data integration and sharing, through its selective loading of data and metadata, while storing the integrated data in a scalable integrated data repository.
△ Less
Submitted 24 April, 2018;
originally announced April 2018.
-
Towards A Systems Approach To Distributed Programming
Authors:
Christopher S. Meiklejohn,
Peter Van Roy
Abstract:
It is undeniable that most developers today are building distributed applications. However, most of these applications are developed by composing existing systems together through unspecified APIs exposed to the application developer. Systems are not going away: they solve a particular problem and most applications today need to rely on several of these systems working in concert. Given this, we p…
▽ More
It is undeniable that most developers today are building distributed applications. However, most of these applications are developed by composing existing systems together through unspecified APIs exposed to the application developer. Systems are not going away: they solve a particular problem and most applications today need to rely on several of these systems working in concert. Given this, we propose a research direction where higher-level languages with well defined semantics target underlying systems infrastructure as a middle-ground.
△ Less
Submitted 7 February, 2018;
originally announced February 2018.
-
An extreme magneto-ionic environment associated with the fast radio burst source FRB 121102
Authors:
D. Michilli,
A. Seymour,
J. W. T. Hessels,
L. G. Spitler,
V. Gajjar,
A. M. Archibald,
G. C. Bower,
S. Chatterjee,
J. M. Cordes,
K. Gourdji,
G. H. Heald,
V. M. Kaspi,
C. J. Law,
C. Sobey,
E. A. K. Adams,
C. G. Bassa,
S. Bogdanov,
C. Brinkman,
P. Demorest,
F. Fernandez,
G. Hellbourg,
T. J. W. Lazio,
R. S. Lynch,
N. Maddox,
B. Marcote
, et al. (9 additional authors not shown)
Abstract:
Fast radio bursts (FRBs) are millisecond-duration, extragalactic radio flashes of unknown physical origin. FRB 121102, the only known repeating FRB source, has been localized to a star-forming region in a dwarf galaxy at redshift z = 0.193, and is spatially coincident with a compact, persistent radio source. The origin of the bursts, the nature of the persistent source, and the properties of the l…
▽ More
Fast radio bursts (FRBs) are millisecond-duration, extragalactic radio flashes of unknown physical origin. FRB 121102, the only known repeating FRB source, has been localized to a star-forming region in a dwarf galaxy at redshift z = 0.193, and is spatially coincident with a compact, persistent radio source. The origin of the bursts, the nature of the persistent source, and the properties of the local environment are still debated. Here we present bursts that show ~100% linearly polarized emission at a very high and variable Faraday rotation measure in the source frame: RM_src = +1.46 x 10^5 rad m^-2 and +1.33 x 10^5 rad m^-2 at epochs separated by 7 months, in addition to narrow (< 30 mus) temporal structure. The large and variable rotation measure demonstrates that FRB 121102 is in an extreme and dynamic magneto-ionic environment, while the short burst durations argue for a neutron star origin. Such large rotation measures have, until now, only been observed in the vicinities of massive black holes (M_BH > 10^4 MSun). Indeed, the properties of the persistent radio source are compatible with those of a low-luminosity, accreting massive black hole. The bursts may thus come from a neutron star in such an environment. However, the observed properties may also be explainable in other models, such as a highly magnetized wind nebula or supernova remnant surrounding a young neutron star.
△ Less
Submitted 11 January, 2018;
originally announced January 2018.
-
Practical Evaluation of the Lasp Programming Model at Large Scale - An Experience Report
Authors:
Christopher S. Meiklejohn,
Vitor Enes,
Junghun Yoo,
Carlos Baquero,
Peter Van Roy,
Annette Bieniusa
Abstract:
Programming models for building large-scale distributed applications assist the developer in reasoning about consistency and distribution. However, many of the programming models for weak consistency, which promise the largest scalability gains, have little in the way of evaluation to demonstrate the promised scalability. We present an experience report on the implementation and large-scale evalua…
▽ More
Programming models for building large-scale distributed applications assist the developer in reasoning about consistency and distribution. However, many of the programming models for weak consistency, which promise the largest scalability gains, have little in the way of evaluation to demonstrate the promised scalability. We present an experience report on the implementation and large-scale evaluation of one of these models, Lasp, originally presented at PPDP `15, which provides a declarative, functional programming style for distributed applications. We demonstrate the scalability of Lasp's prototype runtime implementation up to 1024 nodes in the Amazon cloud computing environment. It achieves high scalability by uniquely combining hybrid gossip with a programming model based on convergent computation. We report on the engineering challenges of this implementation and its evaluation, specifically related to operating research prototypes in a production cloud environment.
△ Less
Submitted 21 August, 2017;
originally announced August 2017.
-
Worlds of Events: Deduction with Partial Knowledge about Causality
Authors:
Seyed Hossein Haeri,
Peter Van Roy,
Carlos Baquero,
Christopher Meiklejohn
Abstract:
Interactions between internet users are mediated by their devices and the common support infrastructure in data centres. Kee** 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 kee** large quantities of metadata; even m…
▽ More
Interactions between internet users are mediated by their devices and the common support infrastructure in data centres. Kee** 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 kee** large quantities of metadata; even more challenging when dealing with resource-limited devices. In this paper, we focus on kee** 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.
△ Less
Submitted 10 August, 2016;
originally announced August 2016.
-
Logic programming in the context of multiparadigm programming: the Oz experience
Authors:
Peter Van Roy,
Per Brand,
Denys Duchier,
Seif Haridi,
Martin Henz,
Christian Schulte
Abstract:
Oz is a multiparadigm language that supports logic programming as one of its major paradigms. A multiparadigm language is designed to support different programming paradigms (logic, functional, constraint, object-oriented, sequential, concurrent, etc.) with equal ease. This article has two goals: to give a tutorial of logic programming in Oz and to show how logic programming fits naturally into…
▽ More
Oz is a multiparadigm language that supports logic programming as one of its major paradigms. A multiparadigm language is designed to support different programming paradigms (logic, functional, constraint, object-oriented, sequential, concurrent, etc.) with equal ease. This article has two goals: to give a tutorial of logic programming in Oz and to show how logic programming fits naturally into the wider context of multiparadigm programming. Our experience shows that there are two classes of problems, which we call algorithmic and search problems, for which logic programming can help formulate practical solutions. Algorithmic problems have known efficient algorithms. Search problems do not have known efficient algorithms but can be solved with search. The Oz support for logic programming targets these two problem classes specifically, using the concepts needed for each. This is in contrast to the Prolog approach, which targets both classes with one set of concepts, which results in less than optimal support for each class. To explain the essential difference between algorithmic and search programs, we define the Oz execution model. This model subsumes both concurrent logic programming (committed-choice-style) and search-based logic programming (Prolog-style). Instead of Horn clause syntax, Oz has a simple, fully compositional, higher-order syntax that accommodates the abilities of the language. We conclude with lessons learned from this work, a brief history of Oz, and many entry points into the Oz literature.
△ Less
Submitted 20 August, 2002;
originally announced August 2002.
