[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*From*: Todd Greenwood-Geer <t.greenwoodgeer@xxxxxxxxx>*Date*: Mon, 20 Apr 2020 13:36:24 -0700 (PDT)

I have a newbie question regarding what is, and is not, an 'atomic' operation in TLA+.

I created a tiny project [here] to capture my question, but it boils down to:

* Are the conjoints within a given action 'atomic'?

* Or alternatively, why is my tla+ code broken :-)

[here] and at bottom of this email.

\* The key action

Increment(p) == /\ v' = v + 1 |

It seems that changes made by one processor are not seen my the other processor.

```
SPECIFICATION Spec
CONSTANT Debug = TRUE
CONSTANT Proc = {p1}
CONSTANT MaxValue = 10
INVARIANTS
Invariants
CONSTRAINTS
ClockConstraint
```

Running this shows a single thread incrementing the single variable `v`

monotonically, as we would expect:

```
$ tlc incrementer.tla
TLC2 Version 2.14 of 10 July 2019 (rev: 0cae24f)
(...)
Computing initial states...
Finished computing initial states: 1 distinct state generated at 2020-04-20 12:29:39.
"Proc[p1] v = 0"
"Proc[p1] v = 1"
"Proc[p1] v = 2"
"Proc[p1] v = 3"
"Proc[p1] v = 4"
"Proc[p1] v = 5"
"Proc[p1] v = 6"
"Proc[p1] v = 7"
"Proc[p1] v = 8"
"Proc[p1] v = 9"
"Proc[p1] v = 10"
Model checking completed. No error has been found.
(...)
```

```
SPECIFICATION Spec
CONSTANT Debug = TRUE
CONSTANT Proc = {p1, p2}
CONSTANT MaxValue = 10
INVARIANTS
Invariants
CONSTRAINTS
ClockConstraint
```

Running this shows what *seems* to be two separate threads incrementing a variable, monotonically, but separately...

```
$ tlc incrementer.tla
TLC2 Version 2.14 of 10 July 2019 (rev: 0cae24f)
Running breadth-first search Model-Checking with fp 17 and seed -6108814598051602586 with 1 worker on 8 cores with 7134MB heap and 64MB offheap memory [pid: 20023] (Linux 4.15.0-96-generic amd64, Ubuntu 11.0.6 x86_64, MSBDiskFPSet, DiskStateQueue).
(...)
Finished computing initial states: 1 distinct state generated at 2020-04-20 12:35:00.
"Proc[p1] v = 0"
"Proc[p2] v = 0"
"Proc[p1] v = 1"
"Proc[p2] v = 1"
"Proc[p1] v = 2"
"Proc[p2] v = 2"
"Proc[p1] v = 3"
"Proc[p2] v = 3"
"Proc[p1] v = 4"
"Proc[p2] v = 4"
"Proc[p1] v = 5"
"Proc[p2] v = 5"
"Proc[p1] v = 6"
"Proc[p2] v = 6"
"Proc[p1] v = 7"
"Proc[p2] v = 7"
"Proc[p1] v = 8"
"Proc[p2] v = 8"
"Proc[p1] v = 9"
"Proc[p2] v = 9"
"Proc[p1] v = 10"
"Proc[p2] v = 10"
Model checking completed. No error has been found.
(...)
```

- Q: Is there really just one instance of the
`v`

variable here? - Q: Is this output some artifact of how PrintT works? Note: I tried moving the print into the
`Increment`

action, and the output is the same:

```
Increment(p) ==
/\ v' = v + 1
/\ PrintT("Proc[" \o ToString(p) \o "] v = " \o ToString(v) \o " to v' = " \o ToString(v'))
```

- Q: From my reading of SpecifyingSystems (page 16), paraphrase, an action is any formula involving primed and unprimed variables. I guess my confusion is w/respect to this... I thought that every action describeda unique point in time. To put it another way, the conjuncts of all the state changes within a given action happen at the same point in time, and are by definition, 'atomic'. It seems that I am misunderstanding something, because if my logic were true, then I would not see p1 and p2 both incrementing from N to N+1 as shown here.

Copy of spec here for completeness:

EXTENDS TLC

PT == INSTANCE PT

LOCAL INSTANCE FiniteSets

LOCAL INSTANCE Sequences

LOCAL INSTANCE Naturals

CONSTANT Debug \* if true then print debug stuff

CONSTANT Proc \* set of processors

CONSTANT MaxValue \* maximum value to increment to

ASSUME DType == Debug \in {TRUE, FALSE}

ASSUME MVType == MaxValue \in Nat

ASSUME ProcType == Cardinality(Proc) > 0

VARIABLES

v \* the single global variable that is

\* being incremented

vars == << v >>

TypeOK == v \in Nat

Invariants == TypeOK

Init == v = 0

Probe(p) ==

IF Debug

THEN PrintT("Proc[" \o ToString(p) \o "] v = " \o ToString(v))

ELSE TRUE

Increment(p) ==

/\ v' = v + 1

/\ Probe(p)

ClockConstraint ==

v <= MaxValue

Next == \E p \in Proc : Increment(p)

Spec == Init /\ [][Next]_vars

=============================================================================

\* Modification History

\* Created by Todd

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+unsubscribe@xxxxxxxxxxxxxxxx.

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/c512cedb-d478-412e-86bf-435f18894e5e%40googlegroups.com.

**Follow-Ups**:**Re: [tlaplus] Is an action atomic?***From:*Markus Kuppe

- Prev by Date:
**Re: [tlaplus] How do you list possible next steps?** - Next by Date:
**Re: [tlaplus] Is an action atomic?** - Previous by thread:
**Re: [tlaplus] TLAPS: problem with proof of GCD from TLA+ Hyperbook (chapter 11.2)** - Next by thread:
**Re: [tlaplus] Is an action atomic?** - Index(es):