Aces4 is a parallel programming platform comprising a DSL for Computational Chemistry and its runtime system. It offers a convenient way to express parallelism together with extensive support for extremely large, possibly sparse, distributed arrays. It aids scientists in the creation of performant, scalable, massively parallel programs that can effectively take advantage of leadership class computing systems to address important scientific questions. Aces4 has enabled the development and implementation of new methods in electronic structure theory which are breaking new ground in their ability to perform highly accurate calculations on ever larger molecular systems. In this paper the design of Aces4, which is based on the the Super Instruction Architecture approach, is described. Experimental scaling results for Molecular Cluster Perturbation Theory, a new method enabled by Aces4, and CCSD, a widely used computational chemistry method are given.

Performance modeling is becoming an increasingly important part of the parallel application development process, particularly for expensive computations that will be run on very high-end systems where resources are scarce. We describe a performance modeling tool SIPMaP (Super Instruction Processor Modeling and Prediction) developed for the Super-Instruction Architecture (SIA). The SIA is designed for applications where the dominant data structures are large multi-dimensional arrays and it comprises a DSL, the Super-Instruction Assembly Language (SIAL) that supports expressing algorithms in terms of blocks (tiles), and its runtime system Super Instruction Processor (SIP) that manages distribution and disk storage of the arrays. SIPMaP generates performance models from the SIAL source code. In comparison with many applications where useful performance models have been developed and reported, these programs are irregular and have other difficult to model characteristics such as extensive overlapping of communication and computation.

According to Java's relaxed memory model, programs that contain data races need not be sequentially consistent. Executions that are not sequentially consistent may exhibit surprising behavior such as operations on a thread occurring in a different order than indicated by the source code or different threads having inconsistent views of updates of shared variables. Java Racefinder (JRF) is an extension of Java Pathfinder (JPF), a model checker for Java bytecode. JRF precisely detects data races as defined by the memory model and can thus be used to verify sequential consistency. We describe an extension to JRF, JRF-Eliminator (JRF-E), that analyzes information collected during model checking, specifically counterexample traces and acquiring histories, and provides advice to the programmer on how to eliminate detected data races from a program. If data races have been eliminated, standard model checking and other verification techniques that implicitly assume sequential consistency can be soundly employed to verify additional properties.

Important classes of problems in computational chemistry, notably coupled cluster methods, consist of solutions to complicated expressions defined in terms of tensors. Tensors are represented by multidimensional arrays that are typically extremely large, thus requiring distribution or in some cases backing on disk. We describe a parallel programming environment, the Super Instruction Architecture (SIA) comprising a domain specific programming language SIAL and its runtime system SIP that are specialized for this class of problems. A novel feature of the programming language is that SIAL programmers express algorithms in terms of operations on blocks rather than individual floating point numbers. Efficient implementations of the block operations as well as management of memory, communication, and I/O are provided by the runtime system. The system has been successfully used to develop ACES III, a software package for computational chemistry.

The Super Instruction Architecture (SIA) was developed to support parallel implementation of algorithms for electronic structure computational chemistry calculations. The methods are programmed in a domain specific programming language called Super Instruction Assembly Language (SIAL). An important novel aspect of SIAL is that algorithms are expressed in terms of operations (super instructions) on blocks (super numbers) rather than individual floating point numbers. The bytecode from compiled SIAL programs is executed by a parallel virtual machine known as the Super Instruction Processor (SIP). Compute intensive operations such as tensor contractions and diagonalizations, as well as communication and I/O are handled by the SIP. By separating the algorithmic complexity of the application domain in SIAL from the complexities of parallel execution on computer hardware in the SIP, a software system has been created that allows for very effective optimization and tuning on different hardware architectures with quite manageable effort.

Most approaches to reasoning about multithreaded programs, including model checking, make the implicit assumption that the system being considered is sequentially consistent. This is, however, invalid in most modern computer architectures and results in unsound reasoning for programs that contain data races, where data races are defined by the memory model of the programming environment. We describe an extension to the model checker Java PathFinder that incorporates knowledge of the Java Memory Model to precisely detect data races in Java byte code. Our tool incorporates special purpose heuristic algorithms that result in shorter counterexample paths. Once data races have been eliminated from a program, Java PathFinder can be soundly employed to verify additional properties.

We describe the ideas behind a method to use assertional reasoning to statically show that all sequentially consistent executions of a concurrent program are free from data races.

Abstract Many parallel programs begin as legacy sequential code that is later reengineered to take advantage of parallel hardware. This paper presents a pattern called Reengineering for Parallelism to help with this task. The new pattern is intended to be used in conjunction with PLPP (Pattern Language for Parallel Programming), described in our book (Mattson TG, Sanders BA, Massingill BL. Patterns for Parallel Programming. Addison‐Wesley: Reading, MA, 2004). PLPP contains a structured collection of patterns and embodies a methodology for developing parallel programs in which the programmer starts with a good understanding of the problem, works through a sequence of patterns, and finally ends up with the code. Most of the patterns in PLPP are also applicable when reengineering legacy code, but it is not always clear how to get started. Reengineering for Parallelism provides an alternate point of entry into PLPP and addresses particular issues that arise when dealing with legacy code. Copyright © 2006 John Wiley & Sons, Ltd.

Abstract The temporal property ‘to-always’ has been proposed for specifying progress properties of concurrent programs. Although the ‘to-always’ properties are a subset of the ‘leads-to’ properties for a given program, ‘to-always’ has more convenient proof rules and in some cases more accurately describes the desired system behavior. In this paper, we give a predicate transformer wta , derive some of its properties, and use it to define ‘to-always’. Proof rules for ‘to-always’ are derived from the properties of wta . We conclude by briefly describing two application areas, nondeterministic data flow networks and self-stabilizing systems where ‘to-always’ properties are useful.

Article Free Access Share on A predicate transformer approach to knowledge and knowledge-based protocols (extended abstract) Author: Beverly Sanders Institut für Computersysteme, Swiss Federal Institute of Technology, (ETH Zürich), ETH Zentrum, CH-8092 Zürich, Switzerland Institut für Computersysteme, Swiss Federal Institute of Technology, (ETH Zürich), ETH Zentrum, CH-8092 Zürich, SwitzerlandView Profile Authors Info & Claims PODC '91: Proceedings of the tenth annual ACM symposium on Principles of distributed computingJuly 1991 Pages 217–230https://doi.org/10.1145/112600.112619Published:01 July 1991Publication History 5citation199DownloadsMetricsTotal Citations5Total Downloads199Last 12 Months5Last 6 weeks1 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteeReaderPDF

Abstract The UNITY substitution axiom, “if (x=y) is an invariant of a program, then x can be replaced by y in any property of the program”, is problematic for several reasons. In this paper, dual predicate transformers sst and wst are introduced that allow the strongest invariant of a program to be expressed, and these are used to give new definitions for the temporal operators unless and ensures . With the new definitions, the substitution axiom is no longer needed, and can be replaced by a derived rule of inference which is formally justified in the logic. One important advantage is that the effects of the initial conditions on the properties of a program are formally captured in a convenient way, and one can forget about substitution in formal treatments of the UNITY proof system while still having it available when desirable to use during the derivation of programs. Composibility and completeness of the modified logic are also discussed.

The dynamic resource sharing that is a characteristic of store-and-forward computer/communication networks allows efficient use of the communication channel but may result in congestion and unfairness with high utilizations. A flow control algorithm is presented to prevent these effects by fairly allocating input rates to the users of the network. The allocation of rates is posed as an optimization problem where users derive a quantifiable benefit (unknown a priori and depending on network performance) from their use of the network. Total benefits are maximized using information reported by the users in a gradient hill climbing algorithm. The incentive problems that arise are examined, and an incentive-compatible pricing mechanism is introduced that prevents strategic manipulation of the algorithm.>

An asynchronous, distributed algorithm is presented that determines the optimal transmission rate allocation in computer networks with virtual circuit routing. The flow control problem is formulated as a gradient hill-climbing algorithm. It is distributed, since the entry node for each virtual circuit iteratively computes the rate allocation for that virtual circuit. The entry node communicates with the associated user during each interaction and obtains information about the rest of the network by sending control packets along the virtual circuit. It is shown that all of the necessary information to solve the optimization problem can be obtained in this fashion and that the algorithm will converge, even though there is no synchronization between nodes and some computations are made with outdated information.>

The concept of an information structure is introduced as a unifying principle behind several of the numerous algorithms that have been proposed for the distributed mutual exclusion problem. This approach allows the development of a generalized mutual exclusion algorithm that accepts a particular information structure at initialization and realizes both known and new algorithms as special cases. Two simple performance metrics of a realized algorithm can be obtained directly from the information structure. A new failure recovery mechanism called local recovery, which requires no coordination between nodes and no additional messages beyond that needed for failure detection, is introduced.