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 Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

The HSA Foundation has produced the HSA Platform System ArchitectureSpecification that goes a long way towards addressing the need for a clear andconsistent method for specifying weakly consistent memory. HSA is specified ina natural language which makes it open to multiple ambiguous interpretationsand could render bugs in implementations of it in hardware and software. Inthis paper we present a formal model of HSA which can be used in thedevelopment and verification of both concurrent software applications as wellas in the development and verification of the HSA-compliant platform itself. Weuse the Event-B language to build a provably correct hierarchy of models fromthe most abstract to a detailed refinement of HSA close to implementationlevel. Our memory models are general in that they represent an arbitrary numberof masters, programs and instruction interleavings. We reason about suchgeneral models using refinements. Using Rodin tool we are able to model andverify an entire hierarchy of models using proofs to establish that eachrefinement is correct. We define an automated validation method that allows usto test baseline compliance of the model against a suite of published HSAlitmus tests. Once we complete model validation we develop a coverage drivenmethod to extract a richer set of tests from the Event-B model and a userspecified coverage model. These tests are used for extensive regression testingof hardware and software systems. Our method of refinement based formalmodelling, baseline compliance testing of the model and coverage driven testextraction using the single language of Event-B is a new way to address a keychallenge facing the design and verification of multi-core systems.

Formal Modelling, Testing and Verification of HSA Memory Models using Event-B