{"body":"// updater\nP0(int *IDX, int *LOCK0, int *UNLOCK0, int *LOCK1, int *UNLOCK1)\n{\n        int lock1;\n        int unlock1;\n        int lock0;\n        int unlock0;\n\n        // SCAN1\n        unlock1 = READ_ONCE(*UNLOCK1);\n        smp_mb(); // A\n        lock1 = READ_ONCE(*LOCK1);\n\n        if (lock1 == unlock1) {\n                // FLIP\n                WRITE_ONCE(*IDX, 1);\n                smp_mb(); // D\n\n                // SCAN2\n                unlock0 = READ_ONCE(*UNLOCK0);\n                smp_mb(); // A\n                lock0 = READ_ONCE(*LOCK0);\n        }\n}\n\n// reader\nP1(int *IDX, int *LOCK0, int *UNLOCK0, int *LOCK1, int *UNLOCK1)\n{\n        int tmp;\n        int idx1;\n        int idx2;\n\n        // 1st reader\n        idx1 = READ_ONCE(*IDX);\n        if (idx1 == 0) {\n                tmp = READ_ONCE(*LOCK0);\n                WRITE_ONCE(*LOCK0, tmp + 1);\n                smp_mb(); /* B and C */\n                tmp = READ_ONCE(*UNLOCK0);\n                WRITE_ONCE(*UNLOCK0, tmp + 1);\n        } else {\n                tmp = READ_ONCE(*LOCK1);\n                WRITE_ONCE(*LOCK1, tmp + 1);\n                smp_mb(); /* B and C */\n                tmp = READ_ONCE(*UNLOCK1);\n                WRITE_ONCE(*UNLOCK1, tmp + 1);\n        }\n\n        // second reader\n        idx2 = READ_ONCE(*IDX);\n        if (idx2 == 0) {\n                tmp = READ_ONCE(*LOCK0);\n                WRITE_ONCE(*LOCK0, tmp + 1);\n                smp_mb(); /* B and C */\n                tmp = READ_ONCE(*UNLOCK0);\n                WRITE_ONCE(*UNLOCK0, tmp + 1);\n        } else {\n                tmp = READ_ONCE(*LOCK1);\n                WRITE_ONCE(*LOCK1, tmp + 1);\n                smp_mb(); /* B and C */\n                tmp = READ_ONCE(*UNLOCK1);\n                WRITE_ONCE(*UNLOCK1, tmp + 1);\n        }\n}\n\nexists (0:lock1=1 /\\ 1:idx1=1 /\\ 1:idx2=1 )  (* bad condition: 1st reader saw flip *)\n","name":"","extension":"txt","url":"https://www.irccloud.com/pastebin/TrXacogO","modified":1671652482,"id":"TrXacogO","size":1858,"lines":66,"own_paste":false,"theme":"","date":1671652482}