Abstract In this paper, we present rIC3, an efficient bit-level hardware model checker primarily based on the IC3 algorithm. It boasts a highly efficient implementation and integrates several recently proposed optimizations, such as the specifically optimized SAT solver, dynamically adjustment of generalization strategies, and the use of predicates with internal signals, among others. As a first-time participant in the Hardware Model Checking Competition, rIC3 was independently evaluated as the best-performing tool, not only in the bit-level track but also in the word-level bit-vector track through bit-blasting. Our experiments further demonstrate significant advancements in both efficiency and scalability. rIC3 can also serve as a backend for verifying industrial RTL designs using SymbiYosys. Additionally, the source code of rIC3 is highly modular, with the IC3 algorithm module being particularly concise, making it an academic platform that is easy to modify and extend.

Abstract The IC3 algorithm, also known as PDR, is a SAT-based model checking algorithm that has significantly influenced the field in recent years due to its efficiency, scalability, and completeness. It utilizes SAT solvers to solve a series of SAT queries associated with relative induction. In this paper, we introduce several optimizations for the SAT solver in IC3 based on our observations of the unique characteristics of these SAT queries. By observing that SAT queries do not necessarily require decisions on all variables, we compute a subset of variables that need to be decided before each solving process while ensuring that the result remains unaffected. Additionally, noting that the overhead of binary heap operations in VSIDS is non-negligible, we replace the binary heap with buckets to achieve constant-time operations. Furthermore, we support temporary clauses without the need to allocate a new activation variable for each solving process, thereby eliminating the need to reset solvers. We developed a novel lightweight CDCL SAT solver, GipSAT, which integrates these optimizations. A comprehensive evaluation highlights the performance improvements achieved by GipSAT. Specifically, the GipSAT-based IC3 demonstrates an average speedup of $$3.61$$ 3.61 times in solving time compared to the IC3 implementation based on MiniSat.

Model checking is an automated method used to formally verify systems by checking them against properties. However, a major problem in model checking is the state explosion. To overcome this challenge, one approach is to utilize parallel processing capabilities to either speed up computations or handle larger-scale problems. Explicit model checking has lower computational complexity and can be easily parallelized. There are numerous parallel explicit model checking algorithms available in the literature. Symbolic model checking offers significant advantages over explicit model checking in terms of problem scalability and verification speed. However, treating states encountered during the search as sets poses a challenge in devising efficient parallel algorithms. As a result, current research on parallelizing symbolic model checking has primarily focused on reachability analysis or safety properties, rather than attempting to parallelize the nested fixpoint calculations. In this paper, we propose a novel property-driven approach for parallel symbolic model checking of full LTL. Our algorithm introduces a fair model state labelling function that forms a partition of the nested fixpoint across the product combining the model and the property Büchi automaton. The experimental results demonstrate significant speedup, ranging from 2.81 to 17.19 times compared to sequential approaches on a 32-core machine. Moreover, in comparison to existing parallel model checking methods, our approach not only surpasses those relying on BDD libraries with a maximum improvement of up to 134% and an average improvement of 33.1% but also demonstrates significant superiority over the state-of-theart parallel explicit model checker.

Design verification is a complex and costly task, especially for large and intricate processor projects. Formal verification techniques provide advantages by thoroughly examining design behaviors, but they require extensive labor and expertise in property formulation. Recent research focuses on verifying designs using the self-consistency universal property, reducing verification difficulty as it is design-independent. However, the single self-consistency property faces false positives and scalability issues due to exponential state space growth. To tackle these challenges, this paper introduces TIUP, a technique using tautologies as universal properties. We show how TIUP effectively uses tautologies as abstract specifications, covering processor data and control paths. TIUP simplifies and streamlines verification for engineers, enabling efficient formal processor verification.

Symbolic quick error detection (SQED) has greatly improved efficiency in formal chip verification. However, it has a limitation in detecting single-instruction bugs due to its reliance on the self-consistency property. To address this, we propose a new variant called symbolic quick error detection by semantically equivalent program execution (SEPE-SQED), which utilizes program synthesis techniques to find sequences with equivalent meanings to original instructions. SEPE-SQED effectively detects single-instruction bugs by differentiating their impact on the original instruction and its semantically equivalent program (instruction sequence). To manage the search space associated with program synthesis, we introduce the CEGIS based on the highest priority first algorithm. The experimental results show that our proposed CEGIS approach improves the speed of generating the desired set of equivalent programs by 50% in time compared to previous methods. Compared to SQED, SEPE-SQED offers a wider variety of instruction combinations and can provide a shorter trace for triggering bugs in certain scenarios.

The IC3 algorithm, also known as PDR, has made a significant impact in the field of safety model checking in recent years due to its high efficiency, scalability, and completeness. The most crucial component of IC3 is inductive generalization, which involves dropping variables one by one and is often the most time-consuming step. In this paper, we propose a novel approach to predict a possible minimal lemma before dropping variables by utilizing the counterexample to propagation (CTP). By leveraging this approach, we can avoid dropping variables if predict successfully. The comprehensive evaluation demonstrates a commendable success rate in lemma prediction and a significant performance improvement achieved by our proposed method.

Software-based distributed shared memory (DSM) allows multiple processes to access shared data without the need for specialized hardware. However, this flexibility comes at a significant cost due to the need for data synchronization. One approach to mitigate these costs is to relax the consistency model, which can lead to delayed updates to the shared data. This approach typically requires the use of explicit synchronization primitives to regulate access to the shared memory and determine the timing of data synchronization. To circumvent the need for explicit synchronization, an alternative approach is to manage shared memory transparently using the underlying system. While this can simplify programming, it often imposes a fixed granularity for data sharing, which can limit the expansion of the coherence domain and increase the synchronization requirements. To overcome this limitation, we propose an abstraction called the elastic coherence domain, which dynamically adjusts the scope of data synchronization and is supported by the underlying system for transparent management of shared memory. The experimental results show that this approach can improve the efficiency of memory sharing in distributed environments.

Speculative execution attacks exploit incorrect speculation to execute malicious instructions and leak data via microarchitectural covert channels. Existing mitigations focus on restricting transmission-related instructions related to covert channels. In this paper, we propose the Execute on Clear (EoC), which offers an efficient defense strategy against covert channels in speculative execution attacks. EoC employs a two-stage identification method, which precisely identifies malicious transmission-related instructions by considering both the insecure data dependency and the status of microarchitecture components exploited by the attack. Moreover, with identification results, EoC guarantees the safe execution of transmission-related instructions, preventing unnecessary blocking. By reducing the misidentification and the blocked execution of such instructions, EoC avoids unnecessary maintenance operations and reduces performance overheads. We evaluate EoC on SPEC2006 and PARSEC3.0 workloads, revealing a performance overhead of merely 0.98% and 3.29% in the Spectre and Futuristic defense models, respectively. Notably, EoC exhibits lower performance overhead in comparison to existing methods.

In recent years, speculative execution attacks bring severe threats to hardware security. An attacker tempts the victim process to read secret data during speculative execution and recovers it via micro-architectural covert channels. Most defense strategies in the literature adopt a blocking approach, in which the execution of malicious speculative instructions is withheld until they become safe and, thus, excessive performance overhead is inevitable. Although several non-blocking approaches have also been proposed, extra hardware components are introduced to buffer data of speculative cache accesses, bringing on significant hardware costs. In this paper, we propose the Secure Access Policy (SAP) to enable the non-blocking execution of malicious speculative instructions in an isolated environment, which reuses the existing Line Fill Buffer and Translation Lookaside Buffer, without introducing any new hardware component. The isolated environment, named Safe Shelter area (SS area), maintains the data accessed by malicious speculative instructions and those data cannot be transmitted to the outside. An improved taint tracking technique is introduced to effectively reduce the number of accesses to the SS area. In addition, an extended cache coherence mechanism and a process-bound technique are also proposed to guarantee the validity and security of SS area’s data. We evaluate SAP on SPEC2006 and PARSEC3.0 workloads. The evaluation results show that SAP can effectively defend those attacks leveraging speculative executions and cache covert channels, and outperforms existing approaches in performance overhead, 2.35% and 3.21% in the Spectre and Futuristic defense models, respectively.

One critical challenge of designing an efficient prefetcher is to strike a balance between performance and hardware overhead. Some state-of-the-art prefetchers achieve very high performance at the price of a very large storage requirement, which makes them not amenable to hardware implementations in commercial processors. We argue that merging memory access patterns can be a feasible solution to reducing storage overhead while obtaining high performance, although no existing prefetchers, to the best of our knowledge, have succeeded in doing so because of the difficulty of designing an effective merging strategy. After analysis of a large number of patterns, we find that the address offset of the first access in a certain memory region is a good feature for clustering highly similar patterns. Based on this observation, we propose a novel hardware data prefetcher, named Pattern Merging Prefetcher (PMP), which achieves high performance at a low cost. The storage requirement for storing patterns is largely reduced and, at the same time, the prefetch accuracy is guaranteed by merging similar patterns in the training process. In the prefetching process, a strategy based on access frequencies of prefetch candidates is applied to accurately extract prefetch targets from merged patterns. According to the experimental results on a wide range of various workloads, PMP outperforms the enhanced Bingo by 2.6% with 30× lesser storage overhead and Pythia by 8.2% with 6× lesser storage overhead.

With the increase in the number of Internet of Things (IoT) devices, more resources can locate at the edge of the Internet. These devices not only collect data about the environment but also affect the environment after certain computations. Conventionally, an IoT application that processes the data provided by devices located in different places, often requires a hierarchical architecture that allows for the data processing and the data collection to occur in different layers. This can be complex for applications requiring direct access to the data provided by remote devices, especially when the data must be exchanged among devices utilizing various machine-to-machine protocols. In this article, an edge service-based architecture is proposed to facilitate the construction of IoT applications. By abstracting the heterogeneous components as virtual devices, it is also possible to construct an IoT application only according to the combination of the virtual devices. The evaluation of the tasks formed by the virtual device shows that it can be efficient to adopt this abstraction method for the utilization of the heterogeneous resources for edge computing.

To learn complex memory access patterns effectively, many spatial data prefetchers have been proposed that characterize the patterns as fixed-length delta sequences. However, because complex patterns are variable in workloads, it is difficult for fixed-length delta sequences to recognize them with both high competitive coverage and accuracy. That is, longer delta sequences increase accuracy at a lower probability of pattern matching, while shorter delta sequences increase coverage at a higher probability of false predictions. A classical strategy is to introduce the multiple matching mechanism associated with variable-length delta sequences, but sequences have to be redundantly stored in multiple tables.

Shared memory is widely used for inter-process communication. The shared memory abstraction allows computation to be decoupled from communication, which offers benefits, including portability and ease of programming. To enable shared memory access by processes that are on different machines, distributed shared memory (DSM) can be employed. However, DSM systems can suffer from thrashing: while different processes update certain hot data items, the largest amount of effort is spent on data synchronization, and little progress is made by each process. To avoid interference between processes during data updating while providing shared memory at page granularity, more time is reserved for a writer to hold a page in a traditional manner. In this paper, we report on complex thrashing, which can explain why extending the time of holding a page might not be sufficient to control thrashing. To increase the throughput, we propose a thrashing control mechanism that allows each process to update a set of pages during a period of time, where the pages compose a logical area. Because of the isolation of areas, updates on different areas can be performed concurrently. To allow the areas to be fairly well used, each process is assigned with a random priority for thrashing control. The thrashing control mechanism is implemented on a Linux-based DSM system. Performance results show that the execution time of the applications that are apt to cause system thrashing can be significantly reduced by our approach.

An issue pertinent to the design of checkpointing protocols is how to improve the autonomy of checkpointing and keep computation loss under control. To address the problem, a time-based multi-cycle checkpointing protocol is proposed in this paper. In this protocol, processes are allowed to take checkpoints with desired checkpoint cycles. To enable recent checkpoints to be used to form a consistent global checkpoint, a communication-based checkpoint cycle adjustment approach is also proposed. In this approach, the checkpoint cycle adjustment of each process follows a P-pattern. Simulation results show that the rollback deviation of the proposed protocol can be well controlled under a low checkpointing overhead.

In a mobile computing system, mobile hosts may move around cells, resulting in a considerable cost for locating and retrieving the recovery information, which is necessary for fault tolerance. To speed up the recovery, traditionally, recovery information is migrated according to the location of the mobile host. In this paper, a scheme for efficiently handling the recovery information is proposed. When a mobile host moves out of a certain range, only partial recovery information of the mobile host needs to be migrated to mobile support stations. It can avoid the unnecessary migration of recovery information. Moreover, the performance of the proposed scheme is evaluated and compared with the traditional movement based scheme.