Commit Graph
297 Commits
Author SHA1 Message Date
Yury Gribov a990595ff0 Added comment in spec. 2025-01-24 11:12:27 +03:00
Yury Gribov 96879fd0a2 Rename variable. 2025-01-24 11:12:27 +03:00
Yury Gribov 2b5d299b7c More automated verification driver. 2025-01-24 11:12:27 +03:00
Yury Gribov f0af663cd0 Minor Promela updates. 2025-01-24 11:12:27 +03:00
Yury Gribov ad6a00dfd1 Added todo. 2025-01-24 11:12:27 +03:00
Yury Gribov e08d19166b Added complaints about Promela. 2025-01-24 11:12:27 +03:00
Yury Gribov 6b9e17be61 Get rid of widths in Promela model. 2025-01-24 11:12:27 +03:00
Yury Gribov 388275accd Added Promela initialization model. 2025-01-24 11:12:27 +03:00
Yury Gribov 40ed720be0 Minor fixes in TLA spec. 2025-01-24 11:12:27 +03:00
Yury Gribov 0f5fc968ff Update spec README. 2025-01-24 11:12:27 +03:00
Yury Gribov 7218f80ef5 Minor spec fix. 2025-01-24 11:12:27 +03:00
Yury Gribov b7acfa4cb7 Minor fixes in tests. 2025-01-24 11:12:27 +03:00
Yury Gribov ea992cb0ae Added simple TLA+ model of Implib.so initialization code. 2025-01-24 11:12:27 +03:00
Yury Gribov 98a7819fd2 Remove redundant barrier. 2025-01-24 11:12:27 +03:00
Yury Gribov 0f95e6b9b5 Updated todo. 2025-01-24 11:12:27 +03:00
Yury Gribov 6c53f2c224 Fix Tsan checks. 2025-01-24 11:12:27 +03:00
Yury Gribov 2dcd486309 Fix Tsan checks. 2025-01-24 11:12:27 +03:00
Yury Gribov 93d62401c5 Added another threading test with deep recursion in library ctor. 2025-01-24 11:12:27 +03:00
Yury Gribov f99925c373 Fixed Tsan test and fix harmless data race. 2025-01-24 11:12:27 +03:00
Yury Gribov ebaae93b21 Added script for fuzz testing via unthread library. 2025-01-24 11:12:27 +03:00
Yury Gribov 2bcad76af6 Fixed test comments 2025-01-24 11:12:27 +03:00
Yury Gribov 8dc7fcbadd Fix race condition between address resolution and library global ctor. 2025-01-24 11:12:27 +03:00
Yury Gribov a75ed9b6e1 Add explicit void in prototypes. 2025-01-24 11:12:27 +03:00
Yury Gribov 9f738f220a Fix memory ordering. 2025-01-24 11:12:27 +03:00
Yury Gribov d9ac8b76eb Updated comment. 2025-01-24 11:12:27 +03:00
Yury Gribov d55bd74634 Print result in threads test. 2025-01-24 11:12:27 +03:00
Yury Gribov a9c7770787 Enable on 32-bit MIPS. 2025-01-24 11:12:27 +03:00
Yury Gribov 634a8380ea Various test improvements. 2025-01-24 11:12:27 +03:00
Yury Gribov 3d4d608c5e Disable thread test on mipsel (can not repro fail locally). 2025-01-24 11:12:27 +03:00
Yury Gribov cf813dc60e Remove volatile. 2025-01-24 11:12:27 +03:00
Yury Gribov 0d02dc2c8d Update README. 2025-01-24 11:12:27 +03:00
Yury Gribov 7d5644fece FreeBSD fixes. 2025-01-24 11:12:27 +03:00
Yury Gribov 5c4ff7fd31 Thread-safe initialization. 2025-01-24 11:12:27 +03:00
Yury Gribov c6ec69e3f5 Remove todo. 2024-12-31 13:25:05 +03:00
Yury Gribov 5df02e37c7 More fixes. 2024-12-31 13:20:34 +03:00
Yury Gribov 73e16df985 Fixed preparation for FreeBSD. 2024-12-31 13:16:46 +03:00
Yury Gribov 6792ee5501 Fixed workflow file. 2024-12-31 13:11:03 +03:00
Yury Gribov 8abb15c86e Enable tests on FreeBSD. 2024-12-29 05:46:18 +03:00
Yury Gribov f9ff166845 Remove irrelevant claim. 2024-05-26 14:40:25 +03:00
Yury Gribov 565cd738f2 Mention that BSDs mostly work. 2024-04-16 00:16:00 +03:00
Yury Gribov dbac8c998c Enable most tests on FreeBSD. 2024-04-16 00:09:22 +03:00
Yury Gribov 051c584779 Fix cross-compiler names. 2024-04-14 19:32:31 +03:00
Yury Gribov c685e8616f Various fixes to enable most tests on BSD. 2024-04-14 19:30:24 +03:00
Yury Gribov 48a2d1413d Fixed CFI directives for MIPS FP regs. 2024-04-11 19:34:34 +03:00
Yury Gribov be4ceb6df7 Minor test fix. 2024-04-11 19:32:25 +03:00
Yury Gribov 305ee2824e Minor test update. 2024-04-10 23:39:34 +03:00
Yury Gribov 11a0ae532a Improve FP argument passing test and fix MIPS register save code. 2024-04-10 23:35:00 +03:00
Yury Gribov 50593e9142 Improve stack arguments test. 2024-04-10 23:05:07 +03:00
Yury Gribov 8eee2d3397 Added note about MIPS vector regs. 2024-04-10 23:00:10 +03:00
Yury Gribov d4c670f02f Simplify test. 2024-04-10 22:58:27 +03:00