[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [tlaplus] Patterns for detecting data race with TLA+?
- From: Hillel Wayne <hwayne@xxxxxxxxx>
- Date: Fri, 27 May 2022 16:45:21 -0500
- Ironport-data: A9a23:PYylUKKWFs0dDNVcFE+RQ5AlxSXFcZb7ZxGr2PjKsXjdYENS1DwFm GQWXzqDOqqONGf9fN0jPN60oR5X6p+AmodgTAYd+CA2RRqmi+KVXIXDdh+Y0wC6d5CYEho/t 63yTvGacajYm1eF/k/F3oDJ9CU6jefSLlbFILas1hpZHGeIcw98z0M68wIFqtQw24LhXlnS4 YiaT/D3YTdJ5RYkagr41IrY8HuDjNyq0N/PlgFWiVhj5TcyplFNZH4tDfnZw0jQHuG4KtWHq 9Prl9lVyI92EyAFUbtJmp6jGqEDryW70QKm0hK6UID66vROS7BbPqsTbJIhhUlrZzqhsMFck NBpsIOJVEQXH4DQwd8saRgIOnQrVUFG0OevzXmXtMWSywjHdCKpzag+Sk4xOoIc96B8BmQmG f4wcmhcKEDewbvonvTmGoGAhex7RCXvFJ8bs2lk0CqaB/Ata7vyHv7q2/AE8RIarJwSOMfhR OM8RgNCRT2bXEJyC38YD5UxmOqnnH7iayYeo1WQzUYyyzODl1YqiuW3WDbTUsWLGsZzh3+Yn 12c8kfpD0gEbPmD8yXQpxpAgceWxX+hMG4IL5W09+VhnUaI7nAXAVsTTkH+oP+ji0f4WtRFK kVS9DBGkEQp3EmiT924Xhrh5XDZ7lgTXN1fF+B84waIokbJ3+qHLkcVY2ZETNk5jdJ1ex0Hy gayrunoVRU65dV5Vkmh3ruTqDqzPw0cImkDeTIIQGM5Dz/L8NFbYvXnHoYLLUKlsjHmMWqvn G3S/UDSk51W3JFbjfzqlbzSq2v0/sChc+Ij2unAsouYAu5RYYekY8mp7gGe46sQaomeSVaFs T4PnM32AAEy4XOly3blrAYlRurBCxO53Nv03QEH834Jq2TFxpJbVdoMiAyS3W8wWir+RRfnY VXIpSRa74JJMX2hYMdfOtzsUJp1k/O7TYy+CJg4i+aihLAhJGdrGwk+NSatM5zFzSDAbIlkZ M3LLpz2ZZrkIfU4lGPeqxghPU8Dn3hinws/tLj0yBOo1bf2WZJmYeZtDbd6VchovMus+V2Lm /4Gbpvi40gBDIXWP3eGmaZOfQFiBSVqWfje9p0HHsbdeFYOMD96UZf5n+h+E7GJaowE/gs+1 izlAhcwJZuWrSavFDhmnVg5N+u+DMkj9yprVcHuVH7xs0UejU+UxP93X/MKkXMProSPFNZ4E KsIfduuGPNKRmiV8jgRd8Cj/oNlcxuviA2UODe9e340eJs5H17F/drtfw3O8igSD3vn7pBn+ OL+iQ6LE4AeQwlCDdrNbK79xV2Gu3VAyvl5WFHFI4UOdUi1qNpqJiX9g+UZOcYJLRmflDKW2 xzHUxgdrOjJ5YQy9YCR16yDqo6oFcp4H1ZbTzGLt+boaXGC8zP6k4FaUeuOcTTMb0/O+f2vN bdP0vXxEPwbh1IV4YdxFrBcy6hhtdbiorltyBs9QCfGYlGtPbNXInec2P5JuKAQlKRSvhG7W x7W99RXYO7bOM7sHFMLHgc9avWf0vUYxmvb4fgveRuo6yhw876KXl9VIgGXzidaKeItYo8ix O4gvu8Q6hC+20pxaY/d0X4L+jTeNGEEXoUmqooeXN3hhD0txwwQepfbECL3vMyCZtgQYEknJ jiY2PjLi7hGnBGQdnMyET3M2rMYi8le/h9Ny1AGKhKCnd+c3q072xhY8DIWSAVJz0UYj7giZ DAzb0Ald7+T+zpIhdRYWzz+EQ92AhDEqFf6zEEElTGEQkT5BGjMN3EAP/2Q9kQVrzBVcjRBo uHKzW/kVSrtLs722SQ2VEF/rOH7Vpl0/wvLl83kRJvVTsVnP2q62/bwJncOsAbtGsgrhUfKj eZt++l0ZKLhMjMIuOswDIzDjeYcTxWNJWpjR/B9/fJZRjqFI27shjXeeVqsfs5tJuDR9RPqA cJZIM8SBQ+10zyDr2xGCKMAf+19kPIzuItQeq/3PXVU9PyQtD10qImW+S/5i2smBd5plIEyM ITMb3WeFmWIgWZP3HTQptJPIGuybNQJOF/m0Oau/LlbHp4Pqrs3I0Q707/xvnLMdQU6r1Sbu wTMY6KQxOtnkNw+k4zpG6RFJgO1NdKjC7jSoV7r64xDPYHVLMPDlwIJsV27bQ5YCr0cBoZsn rOXvd+rgU7Isd7aiYwCd0VtykWI2SmzYAaTGsf+LX0fnCzbHcGxs10M/Ge3LZEPm9RYjiViq 81Ud+PoHeP5mf8ErJGWV8SaOxkaDKvzY6j6oj6ltLKHDR11PcnvMoa87XGwBY1EXnZgBnA9Y zMYf96h4ddXqIlDHhgZH+ogCJh9SLMmtW3KaPWp3QSl4qKUbp9ud1csedfMKd0GN5VcLPvH3 A==
- Ironport-hdrordr: A9a23:mj65gaq4sQTMrIacw8GUHnMaV5t/L9V00zEX/kB9WHVpm5Oj+7 HUoB1L73KE8Ar5BktL6Km90dq7MAThHP9OkPgs1NKZM2fbUQSTXfJfBOfZsnXd8mjFh6VgPU kJSdk7NDXfZWIKyPoSozPIUurJ+bG8geKVbJ7lvjBQpGJRGtNdB7ITMHfULqQVfng3OXNjLu vS2iMvnVPJEgVxH77Legh6YwXanay3qHulW29OO/dA0njDsdqG0t7H+nOjr2Mjul10sMEfGC T+4nnEDmTKiYDe9vYe7R6x032VorrcImspPr3OtiHYEESPtu6kD74RFoFrTFsO0auSAZ8R4b y8xWZeA+1Dr0nJdmXwixrg0Qvt3XIP7DvN0lmFmBLY0IzEeA4=
- Ironport-sdr: JFO3+lYMiX5RaNpgtxEF+3Hevt5tEYTkZ2bjTmaNuLGSPoRTs3WUe9ZlfZPKKoSCReAOC58vrA wHy08C6Nv+t7jiVRX2lv6hw7QCaQ1H56F60T1vyq/RC+q16kuumHTxY1JIw+MSJU49mvevXLoI N/ZzhN47TGdRAiLkjNeV0WZmRNt36v/3YBveK33ayjn3LZEUM43ei4APwuMPMkQxXWCohv4JKM dLhGMhWK2QgzrDEZ0g7lBbciGvVpJD8kqaS6U2VQ0aB+A0KRYlEFwBBJZ/TqKm/CUUQqSYtFg2 Awnr1C65Ie/yGurxDExlJk4u
- References: <c420702c-cd8c-2c58-ca2d-f9d1bd8569d0@shuhaowu.com>
- User-agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:91.0) Gecko/20100101 Thunderbird/91.9.1
Hi Shuhao,
Your spec doesn't necessarily mean the two variables are
reading and writing the same variable at the same time. Remember,
each label represents an abstract amount of time: for all
you know the two actions could be two years apart. It's a good
proxy for bad behavior, but it's still an "indirect" property.
I find that "direct properties" scale better. What is the bad
state that both processes writing at the same time would cause?
If you check that as an invariant, race conditions will
naturally appear in the error trace. You can then write indirect
properties for the specific race conditions you see to make them
trigger earlier in the model checking.
(One useful tool for this is Action
Properties, which let you assert properties on how variables
change in a step.)
H
On 5/27/2022 4:13 PM, Shuhao Wu wrote:
Hello
all:
I'm currently working on some lock-less algorithms with TLA+
(specifically, with PlusCal). One of the things that needs to be
checked is that the algorithm is data-race-free, where no two
processes (in PlusCal terms) are reading and writing to the same
variable at the same time. Here's a sample spec with a data race
on the Global2 variable:
variables Global1 = 0, Global2 = 0;
fair process A = "A"
variable local;
begin
A1:
local := Global1;
A2:
Global2 := 10;
end process;
fair process B = "B"
variable local;
begin
B1:
local := Global1;
B2:
local := Global2;
end process;
Checking if a data race occurred in TLC is technically as simple
as checking the invariant ~(pc["A"] = "A2" /\ pc["B"] = "B2").
However, I suspect this doesn't scale very well to specifications
with more variables and states, as you need to manually enumerate
every write (and read) step for the all "global" variables.
Is there a known pattern somewhere to check for this class of
problems? My quick googling doesn't show anything. Am I
approaching this problem from an incorrect angle?
Thanks,
Shuhao
--
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/6c3f1b9d-7000-1c53-0087-f6882d8afdc9%40gmail.com.