Blockchain networks use consensus mechanisms so that participants can exchange transactions without the need to rely on a trusted third party. Consensus mechanisms using Proof of Work burn significant energy to select a block miner, and this delay limits performance. Other consensus mechanisms such as Proof of Stake or Practical Byzantine Fault Tolerance still designate a single validator to append a block to the chain, preventing blocks from being built and published in parallel. In this article, we introduce a new consensus mechanism, Proof of Descriptor, enabling clients to work together to publish blockchain transactions using a descriptor object which stores information on the cooperative parallel execution of transactions. Proof of Descriptor consensus allows commutative transactions to be mined concurrently. It does not require a single leader to append transactions to the ledger, enabling clients to cooperate on publishing transactions. We also propose a novel graph-based ledger with multiple entry points to facilitate the scalability of Proof of Descriptor, as well as a secure hashing scheme to resist long-range attacks. We demonstrate that our approach is as secure as related works with respect to a malicious leader, 51% attack, and other known blockchain vulnerabilities. Furthermore, our experimental evaluation shows that our approach scales with the size of the network, experiencing up to a 4 \(\times\) improvement in throughput over the fastest sequential blockchain, Solana .

Smart contracts are commonly used on blockchains to define complex behaviors not possible with simple transactions. Miners and validators could achieve significant performance gains by executing smart contracts in parallel, but validators must be able to re-execute the proposed block deterministically. Existing works capture the execution order of concurrently executed transactions using locks, or Software Transactional Memory, enabling validators to re-execute the block deterministically. These approaches can introduce a costly overhead for large blocks, in which many transactions must be compared to deduce their ordering. In this paper, we present a methodology for executing smart contracts concurrently without locks by associating each smart contract state variable with a descriptor, and updating these descriptors with Compare-And-Swap (CAS). Whenever a descriptor is updated, we create a reference to the previous descriptor within the new one. The resulting graph represents all conflicts between transactions, and can be used to deterministically re-execute the transactions in parallel. Our approach captures the ordering between transactions whenever a semantic conflict is detected, eliminating the need to compare lock acquisitions, or timestamps. Additionally, our approach provides a guarantee of Lock-Free progress. In our experimental evaluation, our approach achieves a maximum speedup of 70x against related work when tested on block sizes similar to that of Bitcoin, or Ethereum.

Development of job scheduling algorithms, which directly influence High-Performance Computing (HPC) clusters performance, is hindered because popular scheduling quality metrics, such as Bounded Slowdown, poorly correlate with global scheduling objectives that include job packing efficiency and fairness. This report proposes Area Weighted Response Time, a metric that offers an unbiased representation of job packing efficiency, and presents a class of new metrics, Priority Weighted Specific Response Time, that assess both packing efficiency and fairness of schedules. The provided examples of simulation of scheduling of real workload traces and analysis of the resulting schedules with the help of these metrics and conventional metrics, demonstrate that although Bounded Slowdown can be readily improved by modifying the standard First Come First Served backfilling algorithm and by using existing techniques of estimating job runtime, these improvements are accompanied by significant degradation of job packing efficiency and fairness. In contrast, improving job packing efficiency and fairness over the standard backfilling algorithm, which is designed to target those objectives, is difficult. It requires further algorithm development and more accurate runtime estimation techniques that reduce frequency of underpredictions.

Summary Transactional data structures support threads executing a sequence of operations atomically. Dynamic transactions allow operands to be generated on the fly and allows threads to execute code in between the operations of a transaction, in contrast to static transactions which need to know the operands in advance. A framework called lock‐free transactional transformation (LFTT) allows data structures to run high‐performance transactions, but it only supports static transactions. We present dynamic transactional transformation, an extension to LFTT to add support for dynamic transactions and wait‐free progress while retaining its speed. The thread‐helping scheme of LFTT presents a unique challenge to dynamic transactions. We overcome this challenge by changing the input of LFTT from a list of operations to a function, forcing helping threads to always start at the beginning of the transaction, and allowing threads to skip completed operations through the use of a list of return values. We thoroughly evaluate the performance impact of support for dynamic transactions and wait‐free progress and find that these features do not hurt the performance of LFTT for our test cases.

Summary Wait‐freedom guarantees that all processes complete their operations in a finite number of steps regardless of the delay of any process. Combinatorial topology has been proposed in the literature as a formal verification technique to prove the wait‐free computability of decision tasks. Wait‐freedom is proved through the properties of a static topological structure that expresses all possible combinations of execution paths of the protocol solving the decision task. The practical application of combinatorial topology as a formal verification technique is limited because the existing theory only considers protocols in which the manner of communication between processes is through read‐write memory. This research proposes an extension to the existing theory, called the CAS‐extended model. The extended theory includes Compare‐And‐Swap (CAS) and Load‐Link/Store‐Conditional (LL/SC), which are atomic primitives used to achieve wait‐freedom in state‐of‐the‐art protocols. The CAS‐extended model theory can be used to formally verify wait‐free algorithms used in practice, such as concurrent data structures. We present new definitions detailing the construction of a protocol complex in the CAS‐extended model. As a proof‐of‐concept, we formally verify a wait‐free queue with three processes using the CAS‐extended combinatorial topology.

Job scheduling aims to minimize the turnaround time on the submitted jobs while catering to the resource constraints of High Performance Computing (HPC) systems. The challenge with scheduling is that it must honor job requirements and priorities while actual job run times are unknown. Although approaches have been proposed that use classification techniques or machine learning to predict job run times for scheduling purposes, these approaches do not provide a technique for reducing underprediction, which has a negative impact on scheduling quality. A common cause of underprediction is that the distribution of the duration for a job class is multimodal, causing the average job duration to fall below the expected duration of longer jobs. In this work, we propose the Top Percent predictor, which uses a hierarchical classification scheme to provide better accuracy for job run time predictions than the user-requested time. Our predictor addresses multimodal job distributions by making a prediction that is higher than a specified percentage of the observed job run times. We integrate the Top Percent predictor into scheduling algorithms and evaluate the performance using schedule quality metrics found in literature. To accommodate the user policies of HPC systems, we propose priority metrics that account for job flow time, job resource requirements, and job priority. The experiments demonstrate that the Top Percent predictor outperforms the related approaches when evaluated using our proposed priority metrics.

Architectural imperatives due to the slowing of Moore's Law, the broad acceptance of relaxed semantics and the O(n!) worst case verification complexity of generating sequential histories motivate a new approach to concurrent correctness. Desiderata for a new correctness condition are that it be independent of sequential histories, compositional, flexible as to timing, modular as to semantics and free of inherent locking or waiting. We propose Quantifiability, a novel correctness condition that models a system in vector space to launch a new mathematical analysis of concurrency. The vector space model is suitable for a wide range of concurrent systems and their associated data structures. This paper formally defines quantifiability and demonstrates that quantifiability is compositional and non-blocking. Analysis is facilitated with linear algebra, better supported and of much more efficient time complexity than traditional combinatorial methods.

Emerging byte-addressable Non-Volatile Memories (NVMs) enable persistent memory where process state can be recovered after crashes. To enable applications to rely on persistent data, durable data structures with failure-atomic operations have been proposed. However, they lack the ability to allow users to execute a sequence of operations as transactions. Meanwhile, persistent transactional memory (PTM) has been proposed by adding durability to Software Transactional Memory (STM). However, PTM suffers from high performance overheads and low scalability due to false aborts, logging, and ordering constraints on persistence. In this article, we propose PETRA, a new approach for constructing persistent transactional linked data structures. PETRA natively supports transactions, but unlike PTM, relies on the high-level information from the data structure semantics. This gives PETRA unique advantages in the form of high performance and high scalability. Our experimental results using various benchmarks demonstrate the scalability of PETRA in all workloads and transaction sizes. PETRA outperforms the state-of-the-art PTMs by an order of magnitude in transactions of size greater than one, and demonstrates superior performance in transactions of size one.

The performance of HPC clusters depends on efficient scheduling of jobs. However, modern schedulers generally lack real-time information about resource utilization and require users to provide information, which is seldom accurate, on job requirements. The problem is exacerbated as HPC systems become increasingly more complicated and heterogeneous, which gives rise to new resource constraints (GPU, parallel file system, network bandwidth, burst buffers, etc.) In this work, we integrated data from LDMS, the Lightweight Distributed Metric Service, with Slurm, a popular job scheduler. To demonstrate the capabilities of such integration, we enabled scheduling based on the Lustre file system throughput. We demonstrated benefits of measurement of real-time utilization, prediction of applications requirements from historical data, and finer control of resources, in a preliminary evaluation of scheduling on a cluster of virtual machines. We also identified the possibility of further improving the scheduling efficiency through workload-adaptive scheduling, by adjusting the scheduling based on characteristics of the pending job. We validated the feasibility of this strategy by simulating job executions in our custom-made HPC cluster simulator.

The optimistic concurrency control (OCC) utilized by in-memory databases performs writes on thread-local copies and makes the writes visible upon passing validation. However, high contention workloads suffer from failure of the validation step due to non-semantic memory access conflicts, leading to frequent transaction aborts. In this work, we improve the commit rate of in-memory databases by replacing OCC and the underlying indexing of key-value entries in the Silo database with a lock-free transactional dictionary. To further optimize the transactional commit rate, we present transactional merging, a technique that relaxes the semantic conflict resolution of transactional data structures by merging conflicting operations to reduce aborts. Transactional merging guarantees strict serializability through a strategy that recovers the correct abstract state given that a transaction attempting to merge operations aborts. The experimental evaluation demonstrates that the lock-free transactional dictionary with transactional merging achieves an average speedup of 175% over OCC and the Masstree indexing used in the Silo database for write-dominated workloads on a non-uniform memory access system.

Smart contract transactions demonstrate issues of performance and correctness that application programmers must work around. Although the blockchain consensus mechanism approaches ACID compliance, use cases that rely on frequent state changes are impractical due to the block publishing interval of O(10^1) seconds. The effective isolation level is Read-Committed, only revealing state transitions at the end of the block interval. Values read may be stale and not match program order, causing many transactions to fail when a block is committed. This paper perceives the blockchain as a transactional data structure, using this analogy in the development of a new algorithm, Hash-Mark-Set (HMS), that improves transaction throughput by providing a Read-Uncommitted view of state variables. HMS creates a directed acyclic graph (DAG) from the pending transaction pool. The transaction order derived from the DAG is used to provide a Read-Uncommitted view of the data for new transactions, which enter the DAG as they are received. An implementation of HMS is provided, interoperable with Ethereum and ready for use in smart contracts. Over a wide range of transaction mixes, HMS is demonstrated to improve throughput. A side product of the implementation is a new technique, Runtime Argument Augmentation (RAA), that allows smart contracts to communicate with external data services before submitting a transaction. RAA has use cases beyond HMS and can serve as a lightweight replacement for blockchain oracles.

Concurrent libraries provide data structures whose operations appear to execute atomically when invoked individually. Although these libraries guarantee safety for the data structure operations, the composition of operations may be vulnerable to undefined behavior. The difficulty of reasoning about safety properties in a concurrent environment has led to the development of tools to verify that a concurrent data structure meets a correctness condition. The disadvantage of these tools is that they cannot verify that the composition of concurrent data structure operations respects the intended semantics of the algorithm. Formal logic has been proposed to enable the verification of correctness specifications for a concurrent algorithm. However, a large amount of manual labor is required to fully mechanize the correctness proofs of the concurrent algorithm and each concurrent data structure invoked in the algorithm. In this research, we propose Correctness Condition Specification (CCSpec), the first tool that automatically checks the correctness of a composition of concurrent multi-container operations performed in a non-atomic manner. In addition to checking the correctness of a composition of data structure operations in a concurrent algorithm, CCSpec also checks the correctness of each concurrent data structure utilized in the algorithm. A reference to a container is associated with each method called in a concurrent history to enable the evaluation of correctness for a composition of multiple containers. We develop a lightweight custom specification language that allows the user to define a correctness condition associated with the concurrent algorithm and a correctness condition associated with the concurrent data structures. We demonstrate the practical application of CCSpec by checking the correctness of a concurrent depth-first search utilizing a non-blocking stack, a concurrent breadth-first search utilizing a non-blocking queue, a concurrent shortest path algorithm utilizing a non-blocking priority queue, and a concurrent adjacency list utilizing non-blocking sets.

This paper investigates using compiler technology to automatically convert sequential C++ data abstractions, e.g., queues, stacks, maps, and trees, to concurrent lock-free implementations. By automatically tailoring a number of state-of-the-practice synchronization methods to the underlying sequential implementations of different data structures, our automatically synchronized code can attain performance competitive to that of manually-written concurrent data structures by experts and much better performance than heavier-weight support by software transactional memory (STM).

The following topics are dealt with: cloud computing; resource allocation; queueing theory; optimisation; storage management; cache storage; telecommunication network routing; parallel processing; virtual machines; learning (artificial intelligence).

Compared to threads, tasks are a more fine-grained alternative. The task parallel programming model offers benefits in terms of better performance portability and better load-balancing for problems that exhibit nonuniform workloads. A common scenario of task parallel programming is that a task is recursively decomposed into smaller sub-tasks. Depending on the problem domain, the number of created sub-tasks may be nonuniform, thereby creating potential for significant load imbalances in the system. Dynamic load-balancing mechanisms will distribute the tasks across available threads. The final result of a computation may be modeled as a reduction over the results of all sub-tasks. This article describes a simple, yet effective prototype framework, Blaze-Tasks, for task scheduling and task reductions on shared memory architectures. The framework has been designed with lock-free techniques and generic programming principles in mind. Blaze-Tasks is implemented entirely in C++17 and is thus portable. To load-balance the computation, Blaze-Tasks uses task stealing. To manage contention on a task pool, the number of lock-free attempts to steal a task depends on the distance between thief and pool owner and the estimated number of tasks in a victim’s pool. This article evaluates the Blaze framework on Intel and IBM dual-socket systems using nine benchmarks and compares its performance with other task parallel frameworks. While Cilk outperforms Blaze on Intel on most benchmarks, the evaluation shows that Blaze is competitive with OpenMP and other library-based implementations. On IBM, the experiments show that Blaze outperforms other approaches on most benchmarks.

The growth of High Performance Computer (HPC) systems increases the complexity with respect to understanding resource utilization, system management, and performance issues. While raw performance data is increasingly exposed at the component level, the usefulness of the data is dependent on the ability to do meaningful analysis on actionable timescales. However, current system monitoring infrastructures largely focus on data collection, with analysis performed off-system in post-processing mode. This increases the time required to provide analysis and feedback to a variety of consumers.

In the interests of improving database performance, researchers have considered lock-free data structures for their attractive progress guarantees and scalability. This paper considers the performance of a recently developed lock-free structure, multi-dimensional list (MDList), used as a database index in SOS, a high-performance, object-oriented database. In our tests, we find that MDList outperforms the existing locking structures in multi-threaded workloads. This is the first known use of MDList as an index structure in databases.

Transactional memory simplifies multiprocessor programming by providing the guarantee that a sequential block of code in the form of a transaction will exhibit atomicity and isolation. Transactional data structures offer the same guarantee to concurrent data structures by enabling the atomic execution of a composition of operations. The concurrency control of transactional memory systems preserves atomicity and isolation by detecting read/write conflicts among multiple concurrent transactions. State-of-the-art transactional data structures improve on this concurrency control protocol by providing explicit transaction-level synchronization for only non-commutative operations. Since read/write conflicts are handled by thread-level concurrency control, the correctness of transactional data structures cannot be evaluated according to the read/write histories. This presents a challenge for existing correctness verification techniques for transactional memory, because correctness is determined according to the transitions taken by the transactions in the presence of read/write conflicts. In this article, we present Transactional Correctness tool for Abstract Data Types (TxC-ADT), the first tool that can check the correctness of transactional data structures. TxC-ADT elevates the standard definitions of transactional correctness to be in terms of an abstract data type, an essential aspect for checking correctness of transactions that synchronize only for high-level semantic conflicts. To accommodate a diverse assortment of transactional correctness conditions, we present a technique for defining correctness as a happens-before relation. Defining a correctness condition in this manner enables an automated approach in which correctness is evaluated by generating and analyzing a transactional happens-before graph during model checking. A transactional happens-before graph is maintained on a per-thread basis, making our approach applicable to transactional correctness conditions that do not enforce a total order on a transactional execution. We demonstrate the practical applications of TxC-ADT by checking Lock Free Transactional Transformation and Transactional Data Structure Libraries for serializability, strict serializability, opacity, and causal consistency.

Logarithmic search data structures, such as search trees and skiplists, are fundamental building blocks of many applications. Although the self-balancing binary search trees are among the most ubiquitous sequential search data structures, designing non-blocking rebalancing algorithms is challenging due to the required structural alternation, which may stall other concurrent operations. Skiplists, which probabilistically create multiple levels of shortcuts in an ordered list, provide practical alternatives to balanced search trees. The use of skiplists eliminates the need of rebalancing and ensures amortized logarithmic sequential search time, but concurrency is limited under write-dominated workload because the linkage between multiple distant nodes must be updated. In this paper, we present a linearizable lock-free dictionary design based on a multi-dimensional list (MDList). A node in an MDList arranges its child nodes by their dimensionality and order them by coordinate prefixes. The search operation works by first generating a one-to-one mapping from the scalar keys to a high-dimensional vectors space, then uniquely locating the target position by using the vector as coordinates. Our algorithm guarantees worst-case search time of O(log N) where N is the size of key space. Moreover, the ordering property of the data structure is readily maintained during mutations without rebalancing nor randomization. In our experimental evaluation using a micro-benchmark, our dictionary outperforms the state of the art approaches by as much as 100% when the key universe is large and an average of 30% across all scenarios.

Non-blocking algorithms are a class of algorithms that provide guarantees of progress within a system. These progress guarantees come from the fine-grained synchronization techniques incorporated into their design. There are a number of various non-blocking designs and implementations of concurrent algorithms. However, trade-offs between performance and non-blocking algorithm design decisions are poorly understood. The most common method to measure the performance of non-blocking algorithms is to analyze the number of operations completed over a period of time. Unfortunately, this coarse-grained approach for performance analysis is unable to capture and explain many of the nuances of the behavior of non-blocking algorithms. This can result in a flawed perception of such algorithms, which may lead to a misguided use of them. This work provides a fine-grained approach for the analysis of the design and use of non-blocking algorithms. To support this analysis, we introduce a methodology that enables a user to simulate an application's use of an arbitrary non-blocking algorithm and extract insightful information from the performance results. To better understand the behavior of non-blocking algorithms, we present metrics to measure the effectiveness of the key synchronization and memory management techniques used in non-blocking algorithms. Our analysis combines these new metrics with several well-known hardware metrics to explain key behaviors and develop new insights. To demonstrate the effectiveness of the proposed methodology, we integrate it within the Tervel framework and analyzed Tervel's vector in various use cases. Our experiments show that helping mechanisms negatively impact throughput by increasing misaligned data cache accesses. Furthermore, by studying the correlations between different metrics, we are able to observe the effect of thread interference on the CPU instructions and instruction cache invalidation, and then link the decrease in work completed to this effect. In addition to the provided information, these metrics revealed implementation errors that did not affect correctness but caused increased thread congestion.

Non-blocking data structures allow scalable and thread-safe accesses to shared data. They provide individual operations that appear to execute atomically. However, it is often desirable to execute multiple operations atomically in a transactional manner. Previous solutions, such as software transactional memory (STM) and transactional boosting, manage transaction synchronization in an external layer separated from the data structure's own thread-level concurrency control. Although this reduces programming effort, it leads to overhead associated with additional synchronization and the need to rollback aborted transactions.

The vector is a fundamental data structure, which provides constant-time access to a dynamically-resizable range of elements. Currently, there exist no wait-free vectors. The only non-blocking version supports only a subset of the sequential vector API and exhibits significant synchronization overhead caused by supporting opposing operations. Since many applications operate in phases of execution, wherein each phase only a subset of operations are used, this overhead is unnecessary for the majority of the application. To address the limitations of the non-blocking version, we present a new design that is wait-free, supports more of the operations provided by the sequential vector, and provides alternative implementations of key operations. These alternatives allow the developer to balance the performance and functionality of the vector as requirements change throughout execution. Compared to the known non-blocking version and the concurrent vector found in Intel's TBB library, our design outperforms or provides comparable performance in the majority of tested scenarios. Over all tested scenarios, the presented design performs an average of 4.97 times more operations per second than the non-blocking vector and 1.54 more than the TBB vector. In a scenario designed to simulate the filling of a vector, performance improvement increases to 13.38 and 1.16 times. This work presents the first ABA-free non-blocking vector. Unlike the other non-blocking approach, all operations are wait-free and bounds-checked and elements are stored contiguously in memory.

The throughput of concurrent priority queues is pivotal to multiprocessor applications such as discrete event simulation, best-first search and task scheduling. Existing lock-free priority queues are mostly based on skiplists, which probabilistically create shortcuts in an ordered list for fast insertion of elements. The use of skiplists eliminates the need of global rebalancing in balanced search trees and ensures logarithmic sequential search time on average, but the worst-case performance is linear with respect to the input size. In this paper, we propose a quiescently consistent lock-free priority queue based on a multi-dimensional list that guarantees worst-case search time of O(logN) for key universe of size N. The novel multi-dimensional list (MDList) is composed of nodes that contain multiple links to child nodes arranged by their dimensionality. The insertion operation works by first injectively mapping the scalar key to a high-dimensional vector, then uniquely locating the target position by using the vector as coordinates. Nodes in MDList are ordered by their coordinate prefixes and the ordering property of the data structure is readily maintained during insertion without rebalancing nor randomization. In our experimental evaluation using a micro-benchmark, our priority queue achieves an average of 50 percent speedup over the state of the art approaches under high concurrency.

Identifying design patterns that limit the performance of multi-core algorithms is a challenging task. There are many known methods by which threads synchronize their actions and each method may exhibit different behavior in different use cases. These use cases may vary in regards to the workload being executed, number of parallel tasks, dependencies between these tasks, and the behavior of the system scheduler. Restructuring algorithms to overcome performance limitations requires intimate knowledge on how these algorithms utilize the hardware. In our experience, we have found a lack of adequate tools to gain such knowledge. To address this, we have enhanced and implemented additional data sampler modules for OVIS's Lightweight Distributed Metric Service (LDMS) to enable scalable distributed collection of hardware performance counter data. These modules provide an interface by which LDMS can utilize the PAPI library, Linux perf tools, and RAPL to collect hardware performance data of interest. Using these samplers, we plan to monitor the intra-node behavior, including contention for node level shared resources, of multi-core applications for a diverse set of use cases. We are currently exploring how the values reported are affected by the level of concurrency, the synchronization methodologies, and progress guarantees. We hope to use this information to identify ways to restructure algorithms to increase their performance.

Validation is highly important in parallel application simulations with a large number of parameters, a process that can vary depending on the structure of the simulator and the granularity of the models used. Common practice involves calculating the percentage error between the projected and the real execution time of a benchmark program. However, this coarse-grained approach often suffers from a parameter insensitivity problem in regions of high-dimensional parameter space. In this work we demonstrate the use of our fine-grained validation toolset to capture and compare the statistical characteristics of a parallel application's execution. It is the first toolset to apply fine-grained statistics to large-scale simulation validation, and our experimental evaluation shows that it offers a significant improvement in fidelity when compared to validation using total execution time.

The design of high-performance computing architectures requires performance analysis of large-scale parallel applications to derive various parameters concerning hardware design and software development. The process of performance analysis and benchmarking an application can be done in several ways with varying degrees of fidelity. One of the most cost-effective ways is to do a coarse-grained study of large-scale parallel applications through the use of program skeletons. The concept of a "program skeleton" that we discuss in this paper is an abstracted program that is derived from a larger program where source code that is determined to be irrelevant is removed for the purposes of the skeleton. In this work, we develop a semi-automatic approach for extracting program skeletons based on compiler program analysis. We demonstrate correctness of our skeleton extraction process by comparing details from communication traces, as well as show the performance speedup of using skeletons by running simulations in the SST/macro simulator.

The ABA problem is a fundamental problem to many CAS-based designs. Its significance has increased with the suggested use of CAS as a core atomic primitive for the implementation of portable lock-free algorithms. The ABA problem's occurrence is due to the intricate and complex interactions of the ap

An increasing number of modern real-time systems and the nowadays ubiquitous multicore architectures demand the application of programming techniques for reliable and efficient concurrent synchronization. Some recently developed Compare-And-Swap (CAS) based nonblocking techniques hold the promise of delivering practical and safer concurrency. The ABA problem is a fundamental problem to many CAS-based designs. Its significance has increased with the suggested use of CAS as a core atomic primitive for the implementation of portable lock-free algorithms. The ABA problem's occurrence is due to the intricate and complex interactions of the application's concurrent operations and, if not remedied, ABA can significantly corrupt the semantics of a nonblocking algorithm. The current state of the art leaves the elimination of the ABA hazards to the ingenuity of the software designer. In this work we provide the first systematic and detailed analysis of the ABA problem in lock-free Descriptor-based designs. We study the semantics of Descriptor-based lock-free data structures and propose a classification of their operations that helps us better understand the ABA problem and subsequently derive an effective ABA prevention scheme. Our ABA prevention approach outperforms by a large factor the use of the alternative CAS-based ABA prevention schemes. It offers speeds comparable to the use of the architecture-specific CAS2 instruction used for version counting. We demonstrate our ABA prevention scheme by integrating it into an advanced nonblocking data structure, a lock-free dynamically resizable array.

The dynamic cast operation allows flexibility in the design and use of data management facilities in object- oriented programs. Dynamic cast has an important role in the implementation of the data management services (DMS) of the mission data system project (MDS), the jet propulsion laboratory's experimental work for providing a state-based and goal-oriented unified architecture for testing and development of mission software. DMS is responsible for the storage and transport of control and scientific data in a remote autonomous spacecraft. Like similar operators in other languages, the C++ dynamic cast operator does not provide the timing guarantees needed for hard real-time embedded systems. In a recent study, Gibbs and Stroustrup (G&S) devised a dynamic cast implementation strategy that guarantees fast constant-time performance. This paper presents the definition and application of a co-simulation framework to formally verify and evaluate the G&S fast dynamic casting scheme and its applicability in the mission data system DMS application. We describe the systematic process of model-based simulation and analysis that has lead to performance improvement of the G&S algorithm's heuristics by about a factor of 2.