English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Tools annual

Global: Zendy Free Plan

Global: Zendy Tools monthly

Global: Zendy Plus monthly

Modern multi-core CPUs might execute memory access instructions of programs out-of-order. However, the SPIN model checker does not check out-of-order executions: it only checks in-order executions. We have developed a library for SPIN that enables checking such out-of-order executions with respect to two memory models, the total store ordering (TSO) and the partial store ordering (PSO). This library provides models of variables shared with multiple threads (shared variables), and read and write macros to access them. Nevertheless, this library has three problems. First, although SPIN accepts Linear Temporal Logic (LTL) formulas, which are used for representing properties to be checked such as safety and liveness, our library did not support LTL formulas referring to shared variables. Secondly, guard statements, which are often used for blocking threads while a guard is not executable, cannot refer to shared variables. Finally, the user was unable to specify initial values of shared variables, but they are initialized with zero. As presented herein, we improved the library to resolve these problems. We produced models using our improved library and investigated the library performance.

Improvement of a Library for Model Checking under Weakly Ordered Memory Model with SPIN