<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE article PUBLIC "-//TaxonX//DTD Taxonomic Treatment Publishing DTD v0 20100105//EN" "../../nlm/tax-treatment-NS0.dtd">
<article xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xmlns:xlink="http://www.w3.org/1999/xlink" xmlns:tp="http://www.plazi.org/taxpub" article-type="research-article" dtd-version="3.0" xml:lang="en">
  <front>
    <journal-meta>
      <journal-id journal-id-type="publisher-id">109</journal-id>
      <journal-id journal-id-type="index">urn:lsid:arphahub.com:pub:3dc5f44e-8666-58db-bc76-a455210e8891</journal-id>
      <journal-title-group>
        <journal-title xml:lang="en">JUCS - Journal of Universal Computer Science</journal-title>
        <abbrev-journal-title xml:lang="en">jucs</abbrev-journal-title>
      </journal-title-group>
      <issn pub-type="ppub">0948-695X</issn>
      <issn pub-type="epub">0948-6968</issn>
      <publisher>
        <publisher-name>Journal of Universal Computer Science</publisher-name>
      </publisher>
    </journal-meta>
    <article-meta>
      <article-id pub-id-type="doi">10.3217/jucs-011-05-0661</article-id>
      <article-id pub-id-type="publisher-id">28399</article-id>
      <article-categories>
        <subj-group subj-group-type="heading">
          <subject>Research Article</subject>
        </subj-group>
        <subj-group subj-group-type="scientific_subject">
          <subject>F.3.1 - Specifying and Verifying and Reasoning about Programs</subject>
        </subj-group>
      </article-categories>
      <title-group>
        <article-title>Investigating Atomicity and Observability</article-title>
      </title-group>
      <contrib-group content-type="authors">
        <contrib contrib-type="author" corresp="yes">
          <name name-style="western">
            <surname>Burton</surname>
            <given-names>Jon</given-names>
          </name>
          <email xlink:type="simple">j.i.burton@ncl.ac.uk</email>
          <xref ref-type="aff" rid="A1">1</xref>
        </contrib>
        <contrib contrib-type="author" corresp="no">
          <name name-style="western">
            <surname>Jones</surname>
            <given-names>Cliff B.</given-names>
          </name>
        </contrib>
      </contrib-group>
      <aff id="A1">
        <label>1</label>
        <addr-line content-type="verbatim">University of Newcastle upon Tyne, , United Kingdom</addr-line>
        <institution>University of Newcastle upon Tyne</institution>
        <country>United Kingdom</country>
      </aff>
      <aff id="A2">
        <label>2</label>
        <addr-line content-type="verbatim">Newcastle University, Newcastle, </addr-line>
        <institution>Newcastle University</institution>
        <addr-line content-type="city">Newcastle</addr-line>
      </aff>
      <author-notes>
        <fn fn-type="corresp">
          <p>Corresponding author: Jon Burton (<email xlink:type="simple">j.i.burton@ncl.ac.uk</email>).</p>
        </fn>
        <fn fn-type="edited-by">
          <p>Academic editor: </p>
        </fn>
      </author-notes>
      <pub-date pub-type="collection">
        <year>2005</year>
      </pub-date>
      <pub-date pub-type="epub">
        <day>28</day>
        <month>05</month>
        <year>2005</year>
      </pub-date>
      <volume>11</volume>
      <issue>5</issue>
      <fpage>661</fpage>
      <lpage>686</lpage>
      <uri content-type="arpha" xlink:href="http://openbiodiv.net/700DE46D-1AC3-53AB-AE77-44C7669E3972">700DE46D-1AC3-53AB-AE77-44C7669E3972</uri>
      <uri content-type="zenodo_dep_id" xlink:href="https://zenodo.org/record/6996751">6996751</uri>
      <permissions>
        <copyright-statement>Jon Burton, Cliff B. Jones</copyright-statement>
        <license license-type="creative-commons-attribution" xlink:href="" xlink:type="simple">
          <license-p>This article is freely available under the J.UCS Open Content License.</license-p>
        </license>
      </permissions>
      <abstract>
        <label>Abstract</label>
        <p>Using the fiction of atomicity as a design abstraction and then refining atomicity as we develop an implementation is widely used in areas of concurrent computing such as database systems and transaction processing. In each of these and similar areas, associated notions of correctness are used in order to show that a particular implementation artefact which exhibits concurrency is correct in some sense with respect to a (possibly notional) description which executes with a greater degree of sequentiality. Of crucial importance in the proof and deployment of such notions of correctness is the issue of observability: i.e. in what broad sense do (human or computer) users of a particular implementation artefact observe the effects of its executions. For example, if a human user is allowed to observe directly the execution of a particular concurrent component then he or she will be able to detect the fact of concurrent - and so non-atomic - execution. In general, however, the notion of observability is treated implicitly or not at all. In this paper, we make it explicit and look at the issue of exploring more fully the connections between atomicity and observability. The ultimate aim of this consideration is to work towards constructing a more general framework for (software or hardware) development by refining atomicity.</p>
      </abstract>
    </article-meta>
  </front>
</article>
