synchronization using a component

14 views
Skip to first unread message

Marko Schuetz-Schmuck

unread,
Jun 12, 2019, 2:08:54 PM6/12/19
to tlaplus
Dear All,

I found it interesting that with TLA+ I can have a component that is
responsible of synchronizing the representations of two
threads. https://github.com/MarkoSchuetz/synchronizer

Best regards,

Marko
signature.asc

Amir A.H.S.A

unread,
Jun 12, 2019, 9:37:43 PM6/12/19
to tla...@googlegroups.com
Dear Marko,

May I suggest you make the following modifications to the Synchronizer spec?

1- Change the name "Init" to a more specific name, such as "TSInit" which stands for ThreadSyncInit.

2- Define a next state relation.

3- Define the complete spec in the following form:
TSSpec ==
/\ TSInit
/\ [][TSNext]_<<threadAWaiting, threadBWaiting>>

4- Define an invariant of the new spec, after all we need to know what is the correctness condition of this specification!
Adding this invariant will allow you to check the correctness of your specification by running the TLC model checker.

5- Add descriptive comments to each part of the spec, for example:
(***************************************************************************)
(* An explanation of the action                                            *)
(***************************************************************************)
waitingForB(threadAVars) ==
  threadAWaiting
    => UNCHANGED threadAVars


Best Regards,
AmirHossein


--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@googlegroups.com.
To post to this group, send email to tla...@googlegroups.com.
Visit this group at https://groups.google.com/group/tlaplus.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/87ef3y1xsk.fsf%40tpad-m.i-did-not-set--mail-host-address--so-tickle-me.
For more options, visit https://groups.google.com/d/optout.

Marko Schuetz-Schmuck

unread,
Jun 14, 2019, 9:00:58 AM6/14/19
to tlaplus
had meant to reply to the list, but replied to the author only:

signature.asc

Amir A.H.S.A

unread,
Jun 14, 2019, 9:05:16 AM6/14/19
to tla...@googlegroups.com
Dear Marko,

I suggest defining a constant named "Threads" to represent the two threads:
CONSTANT Threads

I do not quite understand the purpose of the variables in this spec, but I suggest defining the variables "threadWaiting", "threadVars" and "threadActions":

(******************************************************************)
VARIABLES
threadWaiting,  \* threadWaiting[t] is the same as threadTWaiting.
threadVars,   \* threadVars[t] is the same as threadTVars.
threadActions,   \* threadActions[t] is the same as threadTAction.
(******************************************************************)  

Then you can define your next state relation in the following form:

(******************************************************************)  
SyncThreadNext ==
\/ \E t \in Threads :
/\ waitingForThread(t)
/\ thread(t)
(******************************************************************)  

Adding clear and concise comments to a spec is important and necessary, because it will make the future readers of the spec (including the writer herself) very much grateful!

I also assume you are trying to specify the module "Synchronizer" for future use in other specs. A good spec needs to have everything required to understand it inside itself. Hence, perhaps parameterizing specs is not very useful in practice.

Best Regards,
AmirHossein


On Fri, Jun 14, 2019 at 5:30 PM 'Marko Schuetz-Schmuck' via tlaplus <tla...@googlegroups.com> wrote:
had meant to reply to the list, but replied to the author only:

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@googlegroups.com.
To post to this group, send email to tla...@googlegroups.com.
Visit this group at https://groups.google.com/group/tlaplus.

For more options, visit https://groups.google.com/d/optout.
Dear Amir,


"Amir A.H.S.A" <amir.ah...@gmail.com> writes:

> Dear Marko,
>
> May I suggest you make the following modifications to the Synchronizer spec?

thank you very much for taking the time to consider the spec and to
provide your feedback. I share some thoughts on which I would appreciate
further comment.

> 1- Change the name "Init" to a more specific name, such as "TSInit" which
> stands for ThreadSyncInit.

I am not fond of names that heavily abbreviate (magical number 7 plus or
minus 2) and so for this reason I would prefer your suggestion
ThreadSyncInit. To bring it in line with the other prominent name maybe
SyncThreadInit.


> 2- Define a next state relation.

Of course, SyncThreadActions(...) is the next state action. From the way
you suggest using TSNext below I assume you are suggesting hiding the
parameters. I tried parameterization of the Synchronizer in other ways
than with operator parameters, but e.g. substituting CONSTANTS or
VARIABLES:

SYNC == INSTANCE Synchronizer WITH threadAAction <- \E d \in Message: CH!Send(d), threadBAction <- CH!Rcv

results in level errors: CH!Send(...) has level 2.

Any suggestions here in particular?


> 3- Define the complete spec in the following form:
> TSSpec ==
> /\ TSInit
> /\ [][TSNext]_<<threadAWaiting, threadBWaiting>>

Yes, although my SyncThreadNext still has parameters.


> 4- Define an invariant of the new spec, after all we need to know what is
> the correctness condition of this specification!
> Adding this invariant will allow you to check the correctness of your
> specification by running the TLC model checker.

Of course. I am thinking about the correctness and/or liveness
conditions...


> 5- Add descriptive comments to each part of the spec, for example:
> (***************************************************************************)
> (* An explanation of the action
> *)
> (***************************************************************************)
> waitingForB(threadAVars) ==
>   threadAWaiting
>     => UNCHANGED threadAVars

I added some such comments, but they seem to me somewhat redundant,
because to me the definitions (choice of names, ...) seemed
self-documenting, but maybe that comes from being immersed in the
topic...

Thanks again for your feedback,

Marko

> For more options, visit https://groups.google.com/d/optout.

--
Prof. Dr. Marko Schütz-Schmuck
Department of Mathematical Sciences
University of Puerto Rico at Mayagüez
Mayagüez, PR 00681


--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@googlegroups.com.
To post to this group, send email to tla...@googlegroups.com.
Visit this group at https://groups.google.com/group/tlaplus.
Reply all
Reply to author
Forward
0 new messages