[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [tlaplus] Patterns for detecting data race with TLA+?
- From: Shuhao Wu <shuhao@xxxxxxxxxxxx>
- Date: Mon, 30 May 2022 12:58:36 -0400
- Feedback-id: ief094244:Fastmail
- Ironport-data: A9a23:EfpUOKnYkfdFsKQCqOdNyDjo5gwBI0RdPkR7XQ2eYbSJt1+Wr1Gzt xJMCmCFaKqIMzP9f49/aoW38EwAucDczIc3TlM6qXwxRFtH+JHPbTi7BhepbnnKdqUvb2o+s p5AMoGYRCwQZiWBzvt4GuG59RGQ7YnRGvykTrSs1hlZHWeIcg944f5Ys7N/09cAbeSRWVvX4 4uv+JWHYjdJ5hYtWo4qw/LbwP9QlK+q0N8olgRWiSdj4TcyP1FMZH4uDfnZw0nQGuG4LcbmL wr394xVy0uCl/sb5nxJpZ6gGqECaua60QFjERO6UYD66vRJjnRaPqrWqJPwZG8P4whlkeydx /1iv6aLWxolYpbLxt0Af0VpFCtBALVZreqvzXiX6aR/zmXDenrohu1hVQQ4ZN1IvOlwBm5K+ LoTLzVlghKr3brnhuLmDLM124J6fJmD0IA34hmMyRnFCf8+RY3YAK/M7vVz4xUIrZ58PM//Q fRCNwZUVTjqXjdiGmo5KKIPtOivgXb7fjJCr0+Nvuw85G27IAlZieWxaoqNIIfiqcN9mFqJn Hnp1H/ALTYAE+64kSqlzk2Pv7qa9c/8cNtKSOfQGuRRqFGS3WcOEwY+SV+y5/yikAu/XcheI goV/DAvpO487iSWosLVWhS5pDucsUdZVYMAQ6s17waCzqeS6AGcboQZctJfQPMsjvQkWDB27 VjXps7FWQ1ouoKoUW3Io994sgiOESQSKGYDYwoNQg0E/8TvrekPYvTnHoYL/Emd3o2dJN3g/ 9yZhHNh2OhL3Kbnw43+rA+X2Wv9znTcZldtvl2/Y46z0u9uiGeYi2GA7FHa6bNYI9/cQADR7 D4LnM+R6O1IBpaI/MBsfAnvNO71jxpmGGeE6bKKI3XH32j0k5JEVdwOiAyS3G8zbq45lcbBO Sc/Qz956p5JJ2eNZqRqeY+3AMlC5fG+SI+1CqGMNIQePMYZmOq7EMdGNR74M4fFwBhErE3DE crznTuEVitAWfs9llJauc9Mj+J7rszB+Y8jbcmjk07PPUu2a3mSRrMIWGZinchohJ5oVD79q o4HX+PTk0s3eLSnMkH/rNBORXhXcylTLc2m+qR/K7/eSiI7STFJI6GLndsJJdc/94wLzbegw 51IcgoGoLYJrSOXc1zih7EKQOiHYKuTWlplbXV9bAzxgiRLjETGxP53SqbbtIIPrIRLpcOYh dFcEylZKvgQGDnB5RoHapzx8N5reBix3FzcMC2ibzwycIRnWhTSvNTje1K3piUJCyO2s+o4o qGhh1OAGsNYGFo9AZaEcu+rwnOwoWMZxLB4UXzOL4QBY07r6oVrd3H8g6ZvccEBIBnO3BWA0 AOSDUtKrOXBudZvosLJmKCNqJi0VeB5GxMCTWXc6L+3Mwjc/3aimNUfALzRIWGCDG6tofesf +RYyf34IcYrplcSvtouCatvwII/+8Dr++1QwDNiESiZdF+sEL5hfiSL0MQW7f9Ny7ZVtBGMV 1qL68VdPbnVasrpHERIelgqaeOM0fwbgD7P9e9zK0L/vXcl8L2CWERUHh+NlC0MfOAuadh6n 7gs6JwM9giyqhs2KdLa3CpawGKBcy4bWKI9u5BGXYLmh1Z5ylxGZpCAWCb67IvVN4dJO0guZ yeb3e/M3uQMgEXFdHU3GD7G2u8E3cYCvxVDzVkjIVWVm4qa2qVmgkUJqTlnHB5Iyhhn0v5oP jQ5PUNCI6jTrSxjg9JOXjzxFgwQVhmY4VDMzUAUnmnVExuhWmDXcj1vPO+M+FweoW1beTdf8 b6Cz3v9SnPvdcf40SZxAhE1+qC+E4wur1Sc292hBNmPBJIgYDDoqqCpYmUMphT9Bt4pnwvMo uwzpLR8bqjyNCgxpawnCtjKju9JE0/ae2ESE+t8+K4pHH3HfG3g0za5LU3sKNhGIObH8BPlB sFiepBGWxikiHfcriwHHbVeZPh7hvk0/MFEdbTsKmoL9bCYq31mqpXN7m/igGYzR8h11t0gI JjabTOIH2Gd2SlOl2nWoJUWM2a0e4NYNgj13eTw6OpQUpxa4LEqfkY13b+5+X6SNVI/rR6Tu QrCYY7QzvBjmdswxdqySv0bClXmM873WcSJ7Bu374ZEY+TJPJqcrAgSsFTmY1lbMLZ5tw6bT lhRXAMbHX8pvYral0jckpiFUrFGvIC8BboHdM3wK3ZekG2JX8qED97vPYynAcQhrT+fzpDPq 8iEhA+YetkSVNNQy2dSdjBFVR0aDswbq4/+8Diloa3k5gc1iGT6wRDOyZMtRW5ccSAMNpLkD RLsoLCl4dUwQEGgwvMbL6kOPqKU62MPlUfrmxMdeNVY4qSVbou+h4bf
- Ironport-hdrordr: A9a23:ZQqH76tYYYdQH/QRV8XrXvEL7skCToMji2hC6mlwRA09TyXGra ze5MjzhCWY+U8ssS8b86HnBEDyewKVyXcT2/heAV7CZniohILMFu5fBOTZsknd8lLFh51gPM tbAuVD4ZjLfBRHZSiT2njiLz4PqOP3qJxAxt2ui0uEdGlRGvhdBn5Ce1ym+y5NNX577S9TLu vY2iMknUvURZ1NVLX4OpBtZYGqzKyu5emWHG97dmwaBRG1/EmVAfzBYlKlN3ElInByKJgZkF Qt+DaJr5lL3cvLgSM0m1Wjmai/WbPau75+7Q+36vT96A+Dtu4ZD74RHYFqcApFw92H2RIPvJ 30uBEwL61ImgPsV1DwhTeo4hLnwSZrwXf/01PwuwqTneXJABYXT/FMj45YbRfVgnBQwu1U4e Zu8yaiu51bAQioplWD2zDEPCsa1nZdUREZ4K8uZrVkIOluD4N5nMgk5UtQVL0AECj55I1iMO 4rItrb+O8+SyLcU0zk
- Ironport-sdr: L8+dAyq90qpv7+EpsKU74dk4RvjNPuzJJFfHW0xHW6F2Ld18p1s5JhGrzr5gV7Io6GiIe5WJqc 3+zj/8uZuRvycKsX46sFZUpxxSi2g6IVXU9F7dfZmjpj1jlq0EileAs90DN3sOmSojmjzaCT74 nJ0X3t2qEY8a9rVF6UjbCFtis9gMk4buPE27IQeNGUpSt8YT9JmUVz0Jdju4Cf4M8p2Kbb9GlW i0KY/kVQvRWRGaGAWza4cPjoJzhIOnW5+qKxiRGo7C2bryhyZVNNHhgGAFLdDFLQQyN0PxQyxs hojiVbarb49ReojdBwZ2m/ZI
- References: <c420702c-cd8c-2c58-ca2d-f9d1bd8569d0@shuhaowu.com> <6c3f1b9d-7000-1c53-0087-f6882d8afdc9@gmail.com>
- User-agent: Mozilla/5.0 (X11; Linux x86_64; rv:91.0) Gecko/20100101 Thunderbird/91.9.0
Thanks Hillel for the suggestion. Your blog post is also very
enlightening, especially on the forbidden state transition checks that I
also struggled with[1].
For my problem though, the race conditions that occur in real-life seem
difficult to model with TLA directly. For example, if I read/write to a
large (multi-word) variable in something like C/C++ without explicit
synchronization, it can result in a torn-read. Without synchronization,
the compiler may even re-order and/or optimize the statements in
unpredictable (undefined) manners. Since in TLA+, the variable values
are usually abstract values, it seems difficult to me to model the
actual "bad" event.
I suppose what I could do is to create an auxiliary variable that
increments and then decrements with each read and write operation, which
may require splitting the read/write operations into multiple steps for
the aux variable. Then I can use an invariant to assert that the aux
variable never increases above 1 to ensure synchronization is properly
implement. Not 100% sure if this is the simplest approach as I have yet
to test it, but it might be an acceptable work around for this purpose.
Thanks again,
Shuhao
[1] I've worked on an unfinished post detailing my journey on
discovering how to write temporaral properties that specifying
conditions like A leads to B and remains at B, or A leads to B at least
once. Once I get it done, I may ask for more feedback here.
On 2022-05-27 17:45, Hillel Wayne wrote:
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
<https://www.hillelwayne.com/post/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
<mailto: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
<https://groups.google.com/d/msgid/tlaplus/6c3f1b9d-7000-1c53-0087-f6882d8afdc9%40gmail.com?utm_medium=email&utm_source=footer>.
--
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/923db76b-4cb2-1256-9130-0a86641d6c6f%40shuhaowu.com.