Content-Type: multipart/alternative;
 boundary="------------4GaEAgH9tXbSb7ks0rD0Gwkk"
Message-ID: <4bf04616-7f7d-f682-fe3e-e2e185b71b00@lipn.univ-paris13.fr>
Date: Sun, 2 Jul 2023 11:37:20 +0200
MIME-Version: 1.0
User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:102.0) Gecko/20100101
 Thunderbird/102.11.0
Subject: Fwd: ATVA 2023 notification for paper 84
Content-Language: fr, en-US
References: <72b52548-5300-6ba9-d439-9d218db30034@it.uu.se>
To: Yu-Fang Chen <yfc@iis.sinica.edu.tw>, Yu-Fang Chen <gulu0724@gmail.com>
Cc: Sun Jun <sunjunhqq@gmail.com>
From: =?UTF-8?B?w4l0aWVubmUgQW5kcsOp?= <Etienne.Andre@lipn.univ-paris13.fr>
Organization: =?UTF-8?Q?Universit=c3=a9_Sorbonne_Paris_Nord?=
In-Reply-To: <72b52548-5300-6ba9-d439-9d218db30034@it.uu.se>

This is a multi-part message in MIME format.
--------------4GaEAgH9tXbSb7ks0rD0Gwkk
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: quoted-printable

Hi again,

Below Parosh's answer.

=C3=89tienne Andr=C3=A9
Universit=C3=A9 Sorbonne Paris Nord
https://lipn.univ-paris13.fr/~andre/


-------- Message transf=C3=A9r=C3=A9 --------
Sujet=C2=A0: 	Re: ATVA 2023 notification for paper 84
Date=C2=A0: 	Sun, 2 Jul 2023 08:47:19 +0200
De=C2=A0: 	Parosh Abdulla <parosh@it.uu.se>
Pour=C2=A0: 	ATVA 2023 <atva2023@easychair.org>


Dear =C3=89tienne and Sun,

It concerns the overlap with our tacas paper.


* We agree that we should have mentioned the tacas paper and explained
the difference (which is easy to do; please see below).
We forgot to mention the paper. It sounds stupid, and it is, but
unfortunately, that is how it is. We apologize.
Our original goal was to work on the case with transactions when we
started working on this project. However, things got overwhelmingly
difficult, and we decided to work on the transaction-less case for
TACAS. The original version of the paper was written with transactions,
and the TACAS submission is a later version that was rewritten for the
transaction-less case. In the original version, we had discussed only
work related to transactions. When we could solve the issue of
transactions completely and decided to submit to ATVA, this earlier
version was revamped to fill in all the new technical details. However,
we should have (but forgot to) added the TACAS paper in the related work
section. If anything, mentioning the differences with the tacas paper
would have strengthened the paper.

* The contributions of this paper are a substantial extension of the
TACAS submission, handling transactions. Analyzing atomic code has been
an open challenge in stateless model checking for a long time. Even
having simple locks is a challenge. For the first time, this paper
proposes an optimal algorithm for handling transactions over non-trivial
memory models. Therefore, the TACAS paper is a simple, special case of
three of the five models here, where the transactions are single
instructions.
The long appendix in the ATVA submission is also since the proofs
involved in the transactional case are much more involved than what we
had at TACAS. The contributions of this paper are a significant
advancement over the TACAS paper, and there is NO overlap in the
technical parts. For instance:

--- Even though the acronyms of the models (like CC, CCv, and CM) are
the same in both places, we cannot reuse the axiomatic semantics from
the TACAS paper. The reason is that the ATVA submission considers
transactional programs, and the traces of these programs define the rf,
mo relations between transactions and not between events.
--- Likewise, computing the readable and visible sets during the
exploration is significantly more complex when transactions are involved
since transactions are a collection of instructions involving multiple
locations. To check whether the value written to a certain location (say
x) by a transaction t is readable, we also need to check the interplay
of writes and reads on other variables happening in transactions other
than t.


* The TACAS paper has already been presented at ETAPS. The ATVA and
TACAS communities are almost identical. Furthermore, there is a
non-empty intersection between the PCs, so logically, it does not make
sense to hide the TACAS paper. We are almost accused of cheating, which
is not good. In such serious cases, it is good to contact the authors
promptly to hear their points of view.


We apologize again for the mistake. However, stay assured that it was a
mistake rather than malicious behavior.
Please, forward our response to the reviewers and the SC.

Thank you very much for your help and patience.

Best Regards,

Parosh
--------------4GaEAgH9tXbSb7ks0rD0Gwkk
Content-Type: text/html; charset=UTF-8
Content-Transfer-Encoding: quoted-printable

<html>
  <head>

    <meta http-equiv=3D"content-type" content=3D"text/html; charset=3DUTF=
-8">
  </head>
  <body>
    <p>Hi again,</p>
    <p>Below Parosh's answer.<br>
    </p>
    <pre class=3D"moz-signature" cols=3D"72">=C3=89tienne Andr=C3=A9
Universit=C3=A9 Sorbonne Paris Nord
<a class=3D"moz-txt-link-freetext" href=3D"https://lipn.univ-paris13.fr/~=
andre/">https://lipn.univ-paris13.fr/~andre/</a>
</pre>
    <div class=3D"moz-forward-container"><br>
      <br>
      -------- Message transf=C3=A9r=C3=A9 --------
      <table class=3D"moz-email-headers-table" cellspacing=3D"0"
        cellpadding=3D"0" border=3D"0">
        <tbody>
          <tr>
            <th valign=3D"BASELINE" nowrap=3D"nowrap" align=3D"RIGHT">Suj=
et=C2=A0:
            </th>
            <td>Re: ATVA 2023 notification for paper 84</td>
          </tr>
          <tr>
            <th valign=3D"BASELINE" nowrap=3D"nowrap" align=3D"RIGHT">Dat=
e=C2=A0: </th>
            <td>Sun, 2 Jul 2023 08:47:19 +0200</td>
          </tr>
          <tr>
            <th valign=3D"BASELINE" nowrap=3D"nowrap" align=3D"RIGHT">De=C2=
=A0: </th>
            <td>Parosh Abdulla <a class=3D"moz-txt-link-rfc2396E" href=3D=
"mailto:parosh@it.uu.se">&lt;parosh@it.uu.se&gt;</a></td>
          </tr>
          <tr>
            <th valign=3D"BASELINE" nowrap=3D"nowrap" align=3D"RIGHT">Pou=
r=C2=A0: </th>
            <td>ATVA 2023 <a class=3D"moz-txt-link-rfc2396E" href=3D"mail=
to:atva2023@easychair.org">&lt;atva2023@easychair.org&gt;</a></td>
          </tr>
        </tbody>
      </table>
      <br>
      <br>
      Dear =C3=89tienne and Sun,<br>
      <br>
      It concerns the overlap with our tacas paper.<br>
      <br>
      <br>
      * We agree that we should have mentioned the tacas paper and
      explained<br>
      the difference (which is easy to do; please see below).<br>
      We forgot to mention the paper. It sounds stupid, and it is, but<br=
>
      unfortunately, that is how it is. We apologize.<br>
      Our original goal was to work on the case with transactions when
      we<br>
      started working on this project. However, things got
      overwhelmingly<br>
      difficult, and we decided to work on the transaction-less case for<=
br>
      TACAS. The original version of the paper was written with
      transactions,<br>
      and the TACAS submission is a later version that was rewritten for
      the<br>
      transaction-less case. In the original version, we had discussed
      only<br>
      work related to transactions. When we could solve the issue of<br>
      transactions completely and decided to submit to ATVA, this
      earlier<br>
      version was revamped to fill in all the new technical details.
      However,<br>
      we should have (but forgot to) added the TACAS paper in the
      related work<br>
      section. If anything, mentioning the differences with the tacas
      paper<br>
      would have strengthened the paper.<br>
      <br>
      * The contributions of this paper are a substantial extension of
      the<br>
      TACAS submission, handling transactions. Analyzing atomic code has
      been<br>
      an open challenge in stateless model checking for a long time.
      Even<br>
      having simple locks is a challenge. For the first time, this paper<=
br>
      proposes an optimal algorithm for handling transactions over
      non-trivial<br>
      memory models. Therefore, the TACAS paper is a simple, special
      case of<br>
      three of the five models here, where the transactions are single<br=
>
      instructions.<br>
      The long appendix in the ATVA submission is also since the proofs<b=
r>
      involved in the transactional case are much more involved than
      what we<br>
      had at TACAS. The contributions of this paper are a significant<br>
      advancement over the TACAS paper, and there is NO overlap in the<br=
>
      technical parts. For instance:<br>
      <br>
      --- Even though the acronyms of the models (like CC, CCv, and CM)
      are<br>
      the same in both places, we cannot reuse the axiomatic semantics
      from<br>
      the TACAS paper. The reason is that the ATVA submission considers<b=
r>
      transactional programs, and the traces of these programs define
      the rf,<br>
      mo relations between transactions and not between events.<br>
      --- Likewise, computing the readable and visible sets during the<br=
>
      exploration is significantly more complex when transactions are
      involved<br>
      since transactions are a collection of instructions involving
      multiple<br>
      locations. To check whether the value written to a certain
      location (say<br>
      x) by a transaction t is readable, we also need to check the
      interplay<br>
      of writes and reads on other variables happening in transactions
      other<br>
      than t.<br>
      <br>
      <br>
      * The TACAS paper has already been presented at ETAPS. The ATVA
      and<br>
      TACAS communities are almost identical. Furthermore, there is a<br>
      non-empty intersection between the PCs, so logically, it does not
      make<br>
      sense to hide the TACAS paper. We are almost accused of cheating,
      which<br>
      is not good. In such serious cases, it is good to contact the
      authors<br>
      promptly to hear their points of view.<br>
      <br>
      <br>
      We apologize again for the mistake. However, stay assured that it
      was a<br>
      mistake rather than malicious behavior.<br>
      Please, forward our response to the reviewers and the SC.<br>
      <br>
      Thank you very much for your help and patience.<br>
      <br>
      Best Regards,<br>
      <br>
      Parosh<br>
    </div>
  </body>
</html>

--------------4GaEAgH9tXbSb7ks0rD0Gwkk--