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 Tools annual

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 monthly

Global: Zendy Plus monthly

Presents the access of premium content as premium feature

Premium Content

Global: Zendy Plus annual

Global: Zendy Free Plan

We present Porthos, the first tool that discovers porting bugs inperformance-critical code. Porthos takes as input a program and the memorymodels of the source architecture for which the program has been developed andthe target model to which it is ported. If the code is not portable, Porthosfinds a bug in the form of an unexpected execution - an execution that isconsistent with the target but inconsistent with the source memory model.Technically, Porthos implements a bounded model checking method that reducesthe portability analysis problem to satisfiability modulo theories (SMT). Thereare two main problems in the reduction that we present novel and efficientsolutions for. First, the formulation of the portability problem contains aquantifier alternation (consistent + inconsistent). We introduce a formula thatencodes both in a single existential query. Second, the supported memory models(e.g., Power) contain recursive definitions. We compute the required leastfixed point semantics for recursion (a problem that was left open in [47])efficiently in SMT. Finally we present the first experimental analysis ofportability from TSO to Power.

Portability Analysis for Axiomatic Memory Models. PORTHOS: One Tool for all Models