diff --git a/formal-models/.github/dbft2.1_centralizedCV.drawio b/formal-models/.github/dbft2.1_centralizedCV.drawio new file mode 100644 index 00000000..a6a0be13 --- /dev/null +++ b/formal-models/.github/dbft2.1_centralizedCV.drawio @@ -0,0 +1 @@ +7V1bc5s4FP41nrYPyXDHfvQl2e3MdrbT7Hbbp46CsU2LEcU4ifvrVwIJkBAYwjWpp9OJJYQQnKPvfOeCPVGX+6c/AuDvPsC17U4UaRs464m6miiKjP6jDh9sbaYDj7hzftFOifQenbV9YAaGELqh47OdFvQ82wqZPhAE8JEdtoFufhl3FnDtXO9/zjrcxb1TXUr7/7Sd7Y5eSJbIkT2gg0nHYQfW8DHTpd5M1GUAYRh/2j8tbRc/Gfpc4vNuC44mCwtsL6xyAnwP/MWfn/ffNt83D9aHT+a3tXGlksU9APdI7vj9e7Le8EQfQgCP3trG88gTdfG4c0L7zgcWPvqIZIr6duHeJYc30Atvwd5xT6hjCfeOhSa7A94B/flwRwYQucoabjuuu4QuDKKLqTfySr8xUf8hDOAPmx7xoIfOWGxdcMASlPAA+kRxg9yHHYT2U+ETkpPnjrTRhns7DE5oCDlhSh7GKW6qBmk/poKfUWnuMkJXNNIJiG5tk6lTeaAPRCQ1xKPMcuIZVjjL5e3tcjkC4chyn8L59bcx/7b7vAbK9uSv/tWXC+/zFXo+Z4VjrxGakCYMwh3cQg+4N2nvghXf9+PeJ49/iprpKX9B6NMxdhieyCBwDCEr4VgwFKuUujI3SDsjc03C/6KpQRDOMYamIo/6bh385CJJ296ajrCwNjjWPzvHiw+QYTI9jVxTi48yLSSfL3jGa502vyYXQI3VE9M6ZVsf7cBBArYDRvewIMo1D9kREGztsETihlhDA9sFofPAzi9SN3LqR+igKyearZkyizs6O8MBHgPLJidlAZ6bR59xW8TgND++v9xEkfInt9NgP+iC/WC46IEu1s4Dsy+Mn0ds9iJNuzpEgp+jAbLmP0USo8fRpy3569LxjSY6IEVDxz9+sn+iP299pCogOL2j86P7ji/BXhZ1R3fA9o7mptBGfdHrT4Vy8LFU7oH14+gnQrkPBPdT5TYFWPwXuEfskwFM4DpbD8MVggMMGgtsphzEAOfkwN5Zr2OottHNgPtoPowsPt5J0d7SFxN9VYCkZ6FXBLUMhyWXTKnkGUNaYq0Kzat0LZs6C0NxqyG4ySy28cYYbjYHuxM0UsvB6JkqbORUWNrEXCvty8s5p/GO54QOUrxfyPDX0WmAV/ng2I8TrArxCIcefMic4xTugjw/yJKHHfDxuP3TFvtq1xsXPlo7ZKqv0dbYOx4IsaYKSSaj6kh+wdYBgh3B8kZM9+fGwjDa4YiqxlnAPEeUVQFH1LuiiHQTDcoIW2VTDemlNgZ6WZ0RxtTrHCOswBzNhsyxmRaKHJUYKg4+8ITAh23wNtLEKyuWFca/YHv/VpHQdGghkqLr5IOkvRMzBHOZkq3kkkiDvG0x2m6ILuHreTCE3wJ7e3RBEKMttxiTLCH9+46gMgfckh+Kl3ijTKbTyXyeWSF6yHSR8SDKTOL7iU6ZTeY6VvCzD3KIe8rcR7SsM93D8iQKCSPhSTFkF5qYK+mabidiZK7kVogSO6ludsCTxCEmcwwm6skJv1CIR5+/ptYKtVL7hBunTKNH6/SSAxvPMWNCZSmgX01V32BpW8LbzgQukDzAKTOM4EzxdXTWw5E1ndtR8Yzt7q+pyPiCPebM3v0B/0FLvIV85yTJG7xMZHbxOhcJixDFkBuBdwmYlYG3aRhmq/DdvSdr5BTID2z8KO5ssh9+F/9O54BCVgZ38PQxWM+Lg9eZg2dWdPCmgzp4eYho4uAp1K+TVfJBlcscPKQTeycs948uTkep06Gfs1vyVJ6ydktpxe1QevMzGgPlgH5FgrAJ3GZmao6wFUGPBTkeAjk7Usy/boyVtLrpHCY7cSAaVVMUo6QgJdAxcIrYfuN0Ws1cBA08rbKdFOZySy72Uuqn6QrCUgNn7zrwR87BusSBejtJtys2mMSd352nYuY2mBVRg9/OUTEV1lFRp0M7KvkoxL0LrR9zy7L9EGchf2PpGPrQ0qFZ8jZLyZ5Bl2pXiqWeZwu8qBa9yesn412yNCrrZMos3yJuaEq0KAWM/WlNMzLUEQO2Ups8tkizZhW90YIcRlNfgasQmXKFal3XlymF/K1xCRIlN2LeMqyvOrZConJwxQkyWeEC7e2wGq4+adoXrRlHiuwS5ONyaS359m3Dc1PYrZvV4mPibFLr3HD6BkjRcE3Sy8azObN89R9fkGU+s7aZX0bFDGFrCCBM4glCB6xzHEdHP8tFodHUd+bLUWYZW5QeLD5hqhacsILo+m/ztYJvRMWC76KoRT0Pv6iwOC10xGIKM9OcWUT+ao8OginEena2aBYPV0OKppH8APrwANzq678EpXNmr6RiGDFAgwOHVgy9obB7vYv4hTBcMwo7T8wa/Xwphem3FEbgYvVZCsMHjmbVDN2LKIUpNqIdl6EK7fKrK0uld0nN322JKX9N6dgAhmjLQY/Bgjaj+GeLigxTa8fF5Xb/VW+WL3k849ib9ThrvAHyut4Z2dZaItu1tuNAFbkJ9fiaOfKMzPnIwxZjqzuqTEOavlnSezmj6CsNcn6j9SCLfTSkp2JPUl2hMQtZtNNy2+k1J7dyIZc+aySFKjobE5xdvKquvapib2mwxJXO0aoZN0NTpyp5ubkg9Jpct2asdVYSa22L+cnFL0r3XAJFmJ9Sm/kNxPTqLPRC814RzROluLrFSvE45ZxfKpnGrBW/lA8XqfqMnaJyHoebSFO5iQqguCOCKn6uxb5whWSP0gMqlSV76qBSy8kefrYekj8HsLefkf2Riu7pBYfBJk3iXmd8ilxcquxL1QpSwcwMNMXTw27WxmRmX7n70aYVLLBuz7Vk1HJV/FK0utxfl/vg6sXfsHbh6heu/kpApNWXrVpHpFaI+VRXuiHmRkV4q8Knm+aU9TPhDv77KmuP7wVylSrOgPWgiBllWbj6zSVePclUOFCPkFaVDxavVpQxgf2FMVbG55ZTYQX1tUrLBFJ8GUXv47tpBvtiuNay/pcs/xgoZcfvx79yyGqQ5s9QyqQYt9vXDRQuSUW/c7WItfHfyVp3fCkQ9hoWzr/d3FbhwoUJRkd5yVPWNxgTFL2V2w73vwhcQP17fUte/HM4eYnnfw0H3XA46SwfgI30gUggJwCSbMz+KAvtSgWn6FVNZnEaoZFcZxyXVaW8XEVi7exndNS8Ey/4laOxy1WVhpYrB9C6lper3s52Rc30l7FiC57+eJh68z8= \ No newline at end of file diff --git a/formal-models/.github/dbft2.1_centralizedCV.png b/formal-models/.github/dbft2.1_centralizedCV.png new file mode 100644 index 00000000..2b5bde40 Binary files /dev/null and b/formal-models/.github/dbft2.1_centralizedCV.png differ diff --git a/formal-models/.github/dbft2.1_threeStagedCV.drawio b/formal-models/.github/dbft2.1_threeStagedCV.drawio new file mode 100644 index 00000000..4aeeeefe --- /dev/null +++ b/formal-models/.github/dbft2.1_threeStagedCV.drawio @@ -0,0 +1 @@ +7V1tc6O2Fv41nmk/JMM79kfbiW87t9vuNG3u3U87BGObXYwoxom9v76SkQAJ8WIQGCfuTidBCAE6R+c85zkHZaTOt4f/hFaw+QSWjjdSpHXoLkfqw0hRZPg/bAistUM1oB5P7g/SKOHWvbt0dlTHCAAvcgO60Qa+79gR1WaFIXiju62Al3+MJ9vynFzr/9xltIlbx7qUtv/iuOsNuZEs4TNbi3TGDbuNtQRvmSb1caTOQwCi+LftYe54aGbIvMTXLQrOJg8WOn5U5wLwqxXMfnnefl19W73an/40vy6NO2USD/NqeXv8xvhpoyOZghDs/aWDRpFH6uxt40bOU2DZ6OwblChs20RbD59eAT9aWFvXO8KGOdi6NhzsyfJ38MenJ9wBS1XW0LHreXPggfB0M3U+Xyzmc9i+i0Lw3SFnfODDK2Zrz9oh+UmoA5lPdIDfwgkj51A4P3Iy61AXHbB1ovAIu+ALDCynYyLJ+PgtFbssj3HjJiNzRcONFlatdTJ2Kg74C5YIXzqL2X/BzvsCDru9s5Z2/jPQf7+Tc7JwllA78SEIow1YA9/yHtPWWdr6GwABlso3J4qOeNatfQRomTkHN/o/msh7HR99yZx5OOA5Ph0cMwefndCFL+qEpM2HL50ZCB1+yZ5LhzodHbNH7GC01sXaQFagcrpoOUXLGR7aSCtc+6+N68cnFq7nURdmFEw6/ZeoDJrQcoWB8w/2oY17/fjDmH7dPC8tZX0MHv7W5zP/+Q4vosgK105U0s/kK2DoeFbkvtLPwVMmfOln4MInTBR3zGiuYjL6GD8XvipVSTh91jHTLUAddsX3kVWdvo/OGBym/2Rc2h/+Ej9Buj6SOam1ZLgGTTUGZtBWq5Vi2wMwaEZtgyYrAgwaXzrSwKTzKD/oj+bZ0rFCmwxqdCIs1ejV+3CtFZyvSmFV+yNanN/22wDP3LiZs8p7grN0wMDHGR3QJPTvNLQVRsSpYBU4tWF/Ip3jduBl+J5afJY6Eugo6/uxSv9kdOKfNFOmdVunR4jda8495cbRJwxCM+r5uQauhb8edM56MDw4obOl+0qtC+OfPYL1J027250EP4UdZC04nCRGzsPf1vinR/q3GmgHFQ2e//yn8w/88VMAVcUKjz+T8eF7x7egbwubT29Atw7mpeBCvernT4WyC5BUXiz7+z5IhPISct6nzmtybPFv1guMrimDaXnu2kfmCpoDZDRmyE+5MMKd4hNbd7mMTbUDX8Z6OY2HLAsGhHBwfTbSHwosaaXp5ZnaUTZGx7dMItgqT1rirQr9q3QvmzQcVeOjlsbNUKhBWWcMVqud04k1UsuNUUMVNnIqLK0sm74mL+ecxru+G7lQ8X5Ax99Kp/PePgsFNlaA+m0Pa8Qs3a888GZvoOO9h4q+dX0rQnrHhZCU4kJphGvX4uh3Lnp8nBozQxDkU1l/xoF8Kgfx6V0BPrIkLorvhGKjlmBRGwJY7IXBMGoixLYMRjv95AUkFTYvabO2aN37L7sg02cXWD7XLnLQgDlPgVVyPZSNvy62rCusaci2+iACX0NnvfesEFtWxvhKQcGtH5XReDyaTjN3hhNIbh53Iugifs7TJZPRVEdqnX/7ZBgu9ohnpREkae+BCtEYnoSJ2CfKCnf+rKYTiJ5RKp8ncbdvoI5CxHVZBEnMayME6aHnnEEkvT55IF4KQTzIjD1koUe/k+6JjcI+nVD4LVGmTEfQsqZ1ADP5CSJzCJiAJChGaXoiTVbUT1B0CAeumRdqgg64ylKAd9vyR2x+Q+4mv6HpdIAoGzqzorrIV1RgmiHwFzn8gL2lLAwJ2fGKQifD9ctPKFJHt0h//twKGImDbB0/aAmCu2L+qwm84aA9MbD0WieEvwbBdutGOZ2BNkVaXIXOc4A3eVH82pKUe/VewpdB6En7mKfN3bNmvlg2xYIYTqiB4rnhhholwLs01FAmTGJNDKNNoy1CNHfPaOcrN4LQQfP05GBg91GYYVNmmGHt4tSwPoQw8EYNM/EijotJjNw0LhYYKpo1ieTxRYlkXpFYQ0a4AIKxsJ0GJe+Sd0tqqTrg3fQqZyiP5THttxQh3lBhBu2NeFPHQ7C4Q6wMrqGBQyf6ujW4fH0qWELnrY9zOTW2Blgbl9cMm2Zp/9YcXNkUZryBfTLqHw53ThQadyYVChfDneOcaF48YH+f2rYTRKi45ANJR5Z0WjzJYrmYeEheSmSJcAM3dXYFcOqPKG+UOqdz/BFbrkEbfsYJ5xWUihZol5INGmTa9+CwInU6xPXm3XXioS8RD9T9NKYgsdoWvTHuZMyUHnddMawUxhmtuUF49QIU8oKXDTCGVhpablcRlSYrTO5PSPBwp5q0PzU6iB74AdMg0vY3vobP17StY7hW+3xu9MDgHSYhX9WdfG1W1J3N9zP96VgjX5KjMQ9nNvysRZMY09PvVy1KHmLzq9aKSwB4xNf83KxdedUcKignzW7aL5tYTJotNLm+c0A/Xl3n7UpyVO1oOfFesyIBhfJPY4NZQEK85riHBBSXIhmEzxRE6Q+dARtqqRvHH/ZZ6lZEwLyHUre6jkZQaUz/5WnCC/p7r1vr85OEinKdelX03ZSUib/34Ku3xEq+ZlnX2TVc7wWthSCCbgL4o6qMVocFRpX1RYapiaFBNCYzywzQHQvC29wqt5ztV7mmhr3n5ILJRLN9Vhxx1XMyIDB+++6kczBeDLIvljxg6aQJM4IgLK7St9HkcpKL6X5nnklymSUklyikTyisZpyS0hOnxI4Wc0xSEX3kskNxb5nr9Y5QSysMUu5+FIlR68TZnPGRJDUC2Zijh0qtIfFGbSu1PmxxVV0HNKDiKta2X7q4ij81tUB4qS+44ji4iiro7vMrQi6UhtQDm9JKRqGIQ/rwZFHLh+S8rfjXysO7GyfUY2F9CXYpY4E0g6VvxGT5FHlC47Uudk7j7qqttIZrF8zrCa1czDFKmZKYhvttXyD672tPqrKHrKIYc0GkMmoeM75nHpLdFK/XEnS+icyL+NecSCLEF3TmY5A52WEJ5ASAC9ayG1uTpswH0Hob1yRArjIb4atSXrA8uYrY3povVyUv1+sTrNrqy3YRgpWZFavrecHqfS5YbRDbWApKHdy+nOuM3CH7kA+z9pXZAsCo4Plllj+Vz8wLMBd0QwaRfeuakUGZaoJbYmBIoetIeFyqlW+0CMNSzRBTnGD2Vl5K7E1VrKDewoDcDiiG1uOnjnyN5IQBN7zYBC+O+Z4tK1qjI8ly+aCzdtJvw+M25Uw/8qbTrUj3IWzAJvqJuMkAlkhflE71O9vIu0EO4rx9vntM/NxyHUJyHRV/a43Z4k5jP7mrgRqpAcz2EBIepn8KNu6e/rVc9fFf \ No newline at end of file diff --git a/formal-models/.github/dbft2.1_threeStagedCV.png b/formal-models/.github/dbft2.1_threeStagedCV.png new file mode 100644 index 00000000..d0df26d0 Binary files /dev/null and b/formal-models/.github/dbft2.1_threeStagedCV.png differ diff --git a/formal-models/README.md b/formal-models/README.md index f5cecb14..b67520d7 100644 --- a/formal-models/README.md +++ b/formal-models/README.md @@ -112,6 +112,246 @@ configuration: * [TLA⁺ specification](./dbftMultipool/dbftMultipool.tla) * [TLC Model Checker configuration](./dbftMultipool/dbftMultipool___AllGoodModel.launch) +## Proposed dBFT 2.1 models + +Based on the liveness locks scenarios found by the TLC model checker in the +[basic dBFT 2.0 model](#basic-dbft-20-model) we've developed two extensions of +dBFT 2.0 protocol that allow to avoid the liveness lock problem and to preserve +the safety properties of the algorithm. The extensions currently don't have +any code-level implementation and presented as a TLA⁺ specifications ready to be +reviewed and discussed. The improved protocol presented in the extensions will +be referred below as dBFT 2.1. + +We've checked both dBFT 2.1 models with the TLC Model Checker against the same +set of launch configurations that was used to reveal the liveness problems of the +[basic dBFT 2.0 model](#basic-dbft-20-model). The improved models have larger +set of states, thus, the TLC Model Checker wasn't able to finish the liveness +requirements checks for *all* possible states. However, the checks have passed for +a state graph diameter that was large enough to believe the presented models +solve the dBFT 2.0 liveness lock problems. + +### Common `Commit` message improvement note + +Here and below we assume that `Commit` messages should bear preparation hashes +from all nodes that have sent the preparation message (>= `M` but not including +a whole `PrepareRequest`). This quickly synchronizes nodes still at the preparation +stage when someone else collects enough preparations. It at the same time prevents +malicious/byzantine nodes from sending spoofed `Commit` messages. The `Commit` +message size becomes a little bigger, but since it's just hashes it still fits +into a single packet in the vast majority of the cases, so it doesn't really matter. + +### dBFT 2.1 stages-based model + +The basic idea of this model is to split the consensus process into three subsequent +stages marked as `I`, `II` and `III` at the scheme. To perform a transition between +two subsequent stages each consensus node should wait for a set of messages from +at least `M` consensus nodes to be received so that it's possible to complete a full +picture of the neighbours' decisions in the current consensus round. In other words, +no transition can happen unless we have `M` number of messages from the subsequent round, +timers are only set up after we have this number of messages, just to wait for +(potentially) a whole set of them. At the same time, each of the stages has +its own `ChangeView[1,2,3]` message to exit to the next consensus round (view) if +something goes wrong in the current one and there's definitely no ability to +continue consensus process in the current view. Below there's a short description +of each stage. Please, refer to the model scheme and specification for further +details. + +#### Stage I + +Once initialized, consensus node has two ways: +1. Send its `PrepareRequest`/`PrepareResponse` message (and transmit to the + `prepareSent` state). +2. Decide to go to the next view on timeout or any other valid reason (like + transaction missing in the node's mempool or wrong proposal) via sending + `ChangeView1` message (and transmit to the `cv1` state). + +This scheme is quite similar to the basic dBFT 2.0 model except the new type of +`ChangeView` message. After that the node enters stage `I` and waits for consensus +messages of stage `I` (`PrepareRequest` or `PrepareResponse` or `ChangeView1`) +from at least `M` neighbours which is needed to decide about the next actions. +The set of received messages can be arranged in the following way: + +* `M` messages of `ChangeView1` type denote that `M` nodes have decided to change + their view directly after initialization due to invalid/missing `PrepareRequest` + which leads to immediate view changing. This is a "fail fast" route that is the + same as with dBFT 2.0 for the widespread case of missing primary. No additional + delay is added, everything works as usual. +* `M` preparation messages (of type `PrepareRequest` or `PrepareResponse`) with + missing `ChangeView3` denote that the majority of nodes have decided to commit which + denotes the safe transition to stage `II` can be performed and `Commit` message + can safely be sent even if there's `ChangeView1` message in the network. Notice + that `ChangeView3` check is just a protection against node seriously lagging + behind. +* `M` messages each of the type `PrepareRequest` or `PrepareResponse` or `ChangeView1` + where at least one message is of the type `ChangeView1` denote that at least `M` + nodes have reached the stage `I` and the node can safely take further steps. + The additional `| Commit | ≤ F ∪ | CV3 | > 0` condition requires the majority of + nodes not to have the `Commit` message to be sent so that it's still possible to + collect enough `ChangeView[2,3]` messages to change the view in further stages. + If so, then the safe transition to stage `II` can be performed and `ChangeView2` + message can safely be sent. + +#### Stage II + +Once the node has `Commit` or `ChangeView2` message sent, it enters the stage `II` +of the consensus process and waits for at least `M` messages of stage `II` +(`Commit` or `ChangeView2`) to perform the transition to the next stage. The set +of accepted messages can be arranged in the following way: + +* `M` messages of `ChangeView2` type denote that `M` nodes have decided to change + their view directly after entering the stage `II` due to timeout while waiting + for the `Commit` messages which leads to immediate view changing. +* `M` messages of type `Commit` denote that the majority of nodes have decided to + commit which denotes the block can be accepted immediately without entering the + stage `III`. Notice that this is the regular flow of normal dBFT 2.0 consensus, + it also hasn't been changed and proceeds the way it was before. +* `M` messages each of the type `Commit` or `ChangeView2` where not more than `F` + messages are of the type `Commit` denotes that the majority of nodes decided to + change their view after entering the stage `II` and there's not enough `Commit` + messages to create the block (and produce the fork), thus, the safe transition + to stage `III` can be performed and `ChangeView3` message can safely be sent + even if there's `Commit` message in the network. + +In addition, the direct transition from `cv2` state to the `commitSent` state is +added in case if it's clear that there's more than `F` nodes have decided to +commit and no `ChangeView3` message has been received which means that it's possible +to produce block in the current view. This path handles a corner case of missing +stage `I` messages, in fact, because `Commit` messages prove that there are at +least `M` preparation messages exist, but the node went `cv2` path just because +it missed some of them. + +#### Stage III + +Unlike the basic dBFT 2.0 model where consensus node locks on the commit phase, +stage `III` gives the ability to escape from the commit phase via collecting the set +of `M` `ChangeView3` messages. This phase is reachable as soon as at least `M` nodes +has reached the phase `II` (have `ChangeView2` or `Commit` messages sent) and if +there's not enough `Commit` messages (<=`F`) to accept the block. This stage is +added to avoid situation when the node is being locked on the `commitSent` state +whereas the rest of the nodes (>`F`) is willing to go to the next view. + +Here's the scheme of transitions between consensus node states for the improved +dBFT 2.1 stages-based model: + +![dBFT 2.1stages-based model](./.github/dbft2.1_threeStagedCV.png) + +Here you can find the specification file and the basic TLC Model Checker launch +configuration: + +* [TLA⁺ specification](./dbft2.1_threeStagedCV/dbftCV3.tla) +* [TLC Model Checker configuration](./dbft2.1_threeStagedCV/dbftCV3___AllGoodModel.launch) + +### dBFT 2.1 model with the centralized view changes + +The improvement which was taken as a base for this model is taken from the pBFT +algorithm and is as follows. +The consensus process is split into two stages with the following meaning: + +* Stage `I` holds the node states from which it's allowed to transmit to the subsequent + view under assumption that the *new* proposal will be generated (as the basic dBFT 2.0 + model does). +* Stage `II` holds the node states from which it's allowed to perform view change + *preserving* the proposal from the previous view. + +Another vital difference from the basic dBFT 2.0 model is that view changes are +being performed by the node on the `DoCV[1,2]` command (consensus message) sent by the +leader of the target view specified via `DoCV[1,2]` parameters. Below presented +the short description of the proposed consensus process. Please, refer to the +model scheme and specification for further details. + +#### Stage I + +Once initialized at view `v`, the consensus node has two ways: + +1. Send its `PrepareRequest`/`PrepareResponse` message (and transmit to the + `prepareSent` state). +2. Decide to go to the next view `v+1` on timeout or any other valid reason like + transaction missing in the node's mempool via sending `ChangeView1(v+1)` message + (and transmitting to the `cv1 to v'=v+1` state). + +After that the node enters stage `I` and perform as follows: + +* If the node has its `PrepareRequest` or `PrepareResponse` sent: + * If at least `M` preparation messages (including its own) collected, then + it's clear that the majority has proposal for view `v` being accepted as + valid and the node can safely send the `Commit` message and transmit to the + phase `II` (`commitSent` state). + * If there's not enough preparation payloads received from the neighbours for a + long time, then the node is allowed to transmit to the stage `II` via sending + its `ChangeView2` message (and changing its state to the `cv2 to v'=v+1`). It + denotes the node's desire to change view to the next one with the current proposal + to be preserved. +* If the node entered the `cv1 to v'=v+1` state: + * If there's a majority (>=`M`) of `ChangeView1(v+1)` messages and the node is + primary in the view `v+1` then it should send the signal (`DoCV1(v+1)` message) + to the rest of the group to change their view to `v+1` with the new proposal + generated. The rest of the group (backup on `v+1` view that have sent their + `ChangeVeiew1(v+1)` messages) should change their view on `DoCV1(v+1)` receiving. + * If there's a majority (>=`M`) of `ChangeView1(v+1)` messages collected, but + `DoCV1(v+1)` is missing for a long time, then the node is able to "skip" view + `v+1` and send the `ChangeView1(v+2)` message hoping that the primary of `v+2` + will be faster enough to send the `DoCV1(v+2)` signal. The process can be repeated + on timeout for view `v+3`, etc. + * If there's more than `F` nodes that have sent their preparation messages + (and, consequently, announced their desire to transmit to the stage `II` of the + current view rather than to change view), then it's clear that it won't be more than `F` messages + of type `ChangeView1` to perform transition to the next view from the stage `II`. + Thus, the node is allowed to send its `ChangeView2` message (and change its + state to the `cv2 to v'=v+1`). Such situation may happen if the node haven't + proposal received in time (consider valid proposal). + +#### Stage II + +Once the node has entered the stage `II`, the proposal of the current round is +considered to be valid. Depending on the node's state the following decisions are +possible: + +* If the node has its `Commit` sent and is in the `commitSent` state: + * If the majority (>=`M`) of the `Commit` messages has been received, then the + block may be safely accepted for the current proposal. + * If there's not enough `Commit` messages for a long time, then it's legal to + send the `ChangeView2(v+1)` message, transmit to the `cv2 to v'=v+1` state + and decide to go to the next view `v+1` preserving the current proposal + and hoping that it would be possible to collect enough `Commit` messages + for it in the view `v+1`. +* If the node is in the `cv2 to v'=v+1` state then: + * If there's a majority (>=`M`) of `ChangeView2(v+1)` messages and the node is + primary in the view `v+1` then it should send the signal (`DoCV2(v+1)` message) + to the rest of the group to change their view to `v+1` with the old proposal of view `v` + preserved. The rest of the group (backup on `v+1` view that have sent their + `ChangeVeiew2(v+1)` messages) should change their view on `DoCV2(v+1)` receiving. + * If there's a majority (>=`M`) of `ChangeView2(v+1)` messages collected, but + `DoCV2(v+1)` is missing for a long time, then the node is able to "skip" view + `v+1` and send the `ChangeView2(v+2)` message hoping that the primary of `v+2` + will be faster enough to send the `DoCV2(v+2)` signal. The process can be repeated + on timeout for view `v+3`, etc. + * Finally, if the node receives at least `M` messages from the stage `I` at max + `F` of which are preparations (the blue dotted arrow from `cv2 to v'=v+1` to + `cv1 to v'=v+1` state), it has the ability to go back to the `cv1` state to start + the new consensus round with the new proposal. This case is kind of special, + it allows to escape from the deadlock situation when the node is locked on `cv2` + state unable to perform any further steps whereas the rest of the network are + waiting in the `cv1` state. Consider the case of four-nodes network where the + first node is permanently "dead", the primary have sent its `PrepareReauest` + and went to the `cv2` state on the timeout and the rest two nodes are waiting + in the `cv1` state not able to move further. + +It should be noted that "preserving the proposal of view `v` in view `v+1`" means +that the primary of view `v+1` broadcasts the `PrepareRequest` message at view `v+1` +that contains the same set of block's fields (transactions, timestamp, primary, etc) as +the `PrepareRequest` proposed in the view `v` has. + +Here's the scheme of transitions between consensus node states for the improved +dBFT 2.1 model with the centralized view changes process: + +![dBFT 2.1 model with the centralized view changes](./.github/dbft2.1_centralizedCV.png) + +Here you can find the specification file and the basic TLC Model Checker launch +configuration: + +* [TLA⁺ specification](./dbft2.1_centralizedCV/dbftCentralizedCV.tla) +* [TLC Model Checker configuration](./dbft2.1_centralizedCV/dbftCentralizedCV___AllGoodModel.launch) + ## How to run/check the TLA⁺ specification ### Prerequirements @@ -137,5 +377,5 @@ configuration: 5. Open the `Model Overview` window in the TLA⁺ Toolbox and check that behaviour specification, declared constants, invariants and properties of the model are filled in with some values. -6. Press `Run TLC on the model` bottom to start the model checking process and +6. Press `Run TLC on the model` button to start the model checking process and explore the progress in the `Model Checkng Results` window. \ No newline at end of file diff --git a/formal-models/dbft2.1_centralizedCV/dbftCentralizedCV.tla b/formal-models/dbft2.1_centralizedCV/dbftCentralizedCV.tla new file mode 100644 index 00000000..5e1d6260 --- /dev/null +++ b/formal-models/dbft2.1_centralizedCV/dbftCentralizedCV.tla @@ -0,0 +1,507 @@ +-------------------------------- MODULE dbftCentralizedCV -------------------------------- + +EXTENDS + Integers, + FiniteSets + +CONSTANTS + \* RM is the set of consensus node indexes starting from 0. + \* Example: {0, 1, 2, 3} + RM, + + \* RMFault is a set of consensus node indexes that are allowed to become + \* FAULT in the middle of every considered behavior and to send any + \* consensus message afterwards. RMFault must be a subset of RM. An empty + \* set means that all nodes are good in every possible behaviour. + \* Examples: {0} + \* {1, 3} + \* {} + RMFault, + + \* RMDead is a set of consensus node indexes that are allowed to die in the + \* middle of every behaviour and do not send any message afterwards. RMDead + \* must be a subset of RM. An empty set means that all nodes are alive and + \* responding in in every possible behaviour. RMDead may intersect the + \* RMFault set which means that node which is in both RMDead and RMFault + \* may become FAULT and send any message starting from some step of the + \* particular behaviour and may also die in the same behaviour which will + \* prevent it from sending any message. + \* Examples: {0} + \* {3, 2} + \* {} + RMDead, + + \* MaxView is the maximum allowed view to be considered (starting from 0, + \* including the MaxView itself). This constraint was introduced to reduce + \* the number of possible model states to be checked. It is recommended to + \* keep this setting not too high (< N is highly recommended). + \* Example: 2 + MaxView + +VARIABLES + \* rmState is a set of consensus node states. It is represented by the + \* mapping (function) with domain RM and range RMStates. I.e. rmState[r] is + \* the state of the r-th consensus node at the current step. + rmState, + + \* msgs is the shared pool of messages sent to the network by consensus nodes. + \* It is represented by a subset of Messages set. + msgs, + + \* blockAccepted holds the view number when the accepted block's proposal + \* was firstly created for each consensus node. It is represented by a + \* mapping RM -> Nat and needed for InvTwoBlocksAcceptedAdvanced invariant + \* evaluation. + blockAccepted + +\* vars is a tuple of all variables used in the specification. It is needed to +\* simplify fairness conditions definition. +vars == <> + +\* N is the number of validators. +N == Cardinality(RM) + +\* F is the number of validators that are allowed to be malicious. +F == (N - 1) \div 3 + +\* M is the number of validators that must function correctly. +M == N - F + +\* These assumptions are checked by the TLC model checker once at the start of +\* the model checking process. All the input data (declared constants) specified +\* in the "Model Overview" section must satisfy these constraints. +ASSUME + /\ RM \subseteq Nat + /\ N >= 4 + /\ 0 \in RM + /\ RMFault \subseteq RM + /\ RMDead \subseteq RM + /\ Cardinality(RMFault) <= F + /\ Cardinality(RMDead) <= F + /\ Cardinality(RMFault \cup RMDead) <= F + /\ MaxView \in Nat + /\ MaxView <= 2 + +\* RMStates is a set of records where each record holds the node state and +\* the node current view. +RMStates == [ + type: {"initialized", "prepareSent", "commitSent", "blockAccepted", "cv1", "cv2", "bad", "dead"}, + view : Nat + ] +\* Messages is a set of records where each record holds the message type, +\* the message sender, sender's view by the moment when message was sent +\* (view field), sender's view by the first moment the PrepareRequest was +\* originally proposed (sourceView field) and the target view for +\* ChangeView[1,2]/DoChangeView[1,2] messages (targetView field). +Messages == [type : {"PrepareRequest", "PrepareResponse", "Commit", "ChangeView1", "ChangeView2", "DoChangeView1", "DoChangeView2"}, rm : RM, view : Nat, targetView : Nat, sourceView : Nat] + +\* -------------- Useful operators -------------- + +\* IsPrimaryInTheView is an operator defining whether provided node r +\* is primary in the consensus round view from the r's point of view. +\* It is a mapping from RM to the set of {TRUE, FALSE}. +IsPrimaryInTheView(r, view) == view % N = r + +\* IsPrimary is an operator defining whether provided node r is primary +\* for the current round from the r's point of view. It is a mapping +\* from RM to the set of {TRUE, FALSE}. +IsPrimary(r) == IsPrimaryInTheView(r, rmState[r].view) + +\* GetPrimary is an operator defining mapping from round index to the RM that +\* is primary in this round. +GetPrimary(view) == CHOOSE r \in RM : view % N = r + +\* GetNewView returns new view number based on the previous node view value. +\* Current specifications only allows to increment view. +GetNewView(oldView) == oldView + 1 + +\* PrepareRequestSentOrReceived denotes whether there's a PrepareRequest +\* message received from the current round's speaker (as the node r sees it). +PrepareRequestSentOrReceived(r) == Cardinality({msg \in msgs : msg.type = "PrepareRequest"/\ msg.rm = GetPrimary(rmState[r].view) /\ msg.view = rmState[r].view}) /= 0 + +\* -------------- Safety temporal formula -------------- + +\* Init is the initial predicate initializing values at the start of every +\* behaviour. +Init == + /\ rmState = [r \in RM |-> [type |-> "initialized", view |-> 0]] + /\ msgs = {} + /\ blockAccepted = [r \in RM |-> 0] + +\* RMSendPrepareRequest describes the primary node r originally broadcasting PrepareRequest. +RMSendPrepareRequest(r) == + /\ rmState[r].type = "initialized" + /\ IsPrimary(r) + /\ rmState' = [rmState EXCEPT ![r].type = "prepareSent"] + /\ msgs' = msgs \cup {[type |-> "PrepareRequest", rm |-> r, view |-> rmState[r].view, targetView |-> 0, sourceView |-> rmState[r].view]} + /\ UNCHANGED <> + +\* RMSendPrepareResponse describes non-primary node r receiving PrepareRequest from +\* the primary node of the current round (view) and broadcasting PrepareResponse. +\* This step assumes that PrepareRequest always contains valid transactions and +\* signatures. +RMSendPrepareResponse(r) == + /\ rmState[r].type = "initialized" + /\ \neg IsPrimary(r) + /\ PrepareRequestSentOrReceived(r) + /\ LET pReq == CHOOSE msg \in msgs : msg.type = "PrepareRequest" /\ msg.rm = GetPrimary(rmState[r].view) /\ msg.view = rmState[r].view + IN /\ rmState' = [rmState EXCEPT ![r].type = "prepareSent"] + /\ msgs' = msgs \cup {[type |-> "PrepareResponse", rm |-> r, view |-> rmState[r].view, targetView |-> 0, sourceView |-> pReq.sourceView]} + /\ UNCHANGED <> + + +\* RMSendCommit describes node r sending Commit if there's enough PrepareResponse +\* messages. +RMSendCommit(r) == + /\ rmState[r].type = "prepareSent" + /\ Cardinality({ + msg \in msgs : (msg.type = "PrepareResponse" \/ msg.type = "PrepareRequest") /\ msg.view = rmState[r].view + }) >= M + /\ PrepareRequestSentOrReceived(r) + /\ LET pReq == CHOOSE msg \in msgs : msg.type = "PrepareRequest" /\ msg.rm = GetPrimary(rmState[r].view) /\ msg.view = rmState[r].view + IN /\ rmState' = [rmState EXCEPT ![r].type = "commitSent"] + /\ msgs' = msgs \cup {[type |-> "Commit", rm |-> r, view |-> rmState[r].view, targetView |-> 0, sourceView |-> pReq.sourceView]} + /\ UNCHANGED <> + +\* RMAcceptBlock describes node r collecting enough Commit messages and accepting +\* the block. +RMAcceptBlock(r) == + /\ rmState[r].type /= "bad" + /\ rmState[r].type /= "dead" + /\ rmState[r].type /= "blockAccepted" + /\ PrepareRequestSentOrReceived(r) + /\ Cardinality({msg \in msgs : msg.type = "Commit" /\ msg.view = rmState[r].view}) >= M + /\ LET pReq == CHOOSE msg \in msgs : msg.type = "PrepareRequest" /\ msg.rm = GetPrimary(rmState[r].view) /\ msg.view = rmState[r].view + IN /\ rmState' = [rmState EXCEPT ![r].type = "blockAccepted"] + /\ blockAccepted' = [blockAccepted EXCEPT ![r] = pReq.sourceView] + /\ UNCHANGED <> + +\* FetchBlock describes node r that fetches the accepted block from some other node. +RMFetchBlock(r) == + /\ rmState[r].type /= "bad" + /\ rmState[r].type /= "dead" + /\ rmState[r].type /= "blockAccepted" + /\ \E rmAccepted \in RM : /\ rmState[rmAccepted].type = "blockAccepted" + /\ rmState' = [rmState EXCEPT ![r].type = "blockAccepted", ![r].view = rmState[rmAccepted].view] + /\ blockAccepted' = [blockAccepted EXCEPT ![r] = blockAccepted[rmAccepted]] + /\ UNCHANGED <> + +\* RMSendChangeView1 describes node r sending ChangeView1 message on timeout +\* during waiting for PrepareResponse or node r in "cv2" state receiving M +\* messages from the I stage not more than F of them are preparations. +RMSendChangeView1(r) == + /\ \/ /\ rmState[r].type = "initialized" + /\ \neg IsPrimary(r) + \/ /\ rmState[r].type = "cv2" + /\ Cardinality({msg \in msgs : /\ (msg.type = "ChangeView1" \/ msg.type = "PrepareRequest" \/ msg.type = "PrepareResponse") + /\ msg.view = rmState[r].view + }) >= M + /\ Cardinality({msg \in msgs : /\ (msg.type = "PrepareRequest" \/ msg.type = "PrepareResponse") + /\ msg.view = rmState[r].view + }) <= F + /\ rmState' = [rmState EXCEPT ![r].type = "cv1"] + /\ msgs' = msgs \cup {[type |-> "ChangeView1", rm |-> r, view |-> rmState[r].view, targetView |-> GetNewView(rmState[r].view), sourceView |-> rmState[r].view]} + /\ UNCHANGED <> + +\* RMSendChangeView1FromCV1 describes node r sending ChangeView1 message on timeout +\* during waiting for DoCV1 signal from the next primary. +RMSendChangeView1FromCV1(r) == + /\ rmState[r].type = "cv1" + /\ LET cv1s == {msg \in msgs : msg.type = "ChangeView1" /\ msg.view = rmState[r].view} + myCV1s == {msg \in cv1s : msg.rm = r} + myBestCV1 == CHOOSE msg \in myCV1s : \A other \in myCV1s : msg.targetView >= other.targetView + IN /\ Cardinality({msg \in cv1s : msg.targetView = myBestCV1.targetView}) >= M + /\ \neg IsPrimaryInTheView(r, myBestCV1.targetView) + /\ msgs' = msgs \cup {[type |-> "ChangeView1", rm |-> r, view |-> rmState[r].view, targetView |-> GetNewView(myBestCV1.targetView), sourceView |-> rmState[r].view]} + /\ UNCHANGED <> + +\* RMSendChangeView2 describes node r sending ChangeView message on timeout +\* during waiting for enough Prepare messages OR from CV1 after not receiving +\* enough ChangeView1 messages. +RMSendChangeView2(r) == + /\ \/ rmState[r].type = "prepareSent" + \/ rmState[r].type = "commitSent" + \/ /\ rmState[r].type = "cv1" + /\ Cardinality({msg \in msgs : /\ (msg.type = "PrepareRequest" \/ msg.type = "PrepareResponse" \/ msg.type = "ChangeView1") + /\ msg.view = rmState[r].view + /\ (msg.targetView = 0 \/ msg.targetView = GetNewView(rmState[r].view)) + }) >= M + /\ Cardinality({msg \in msgs : /\ (msg.type = "PrepareRequest" \/ msg.type = "PrepareResponse") + /\ msg.view = rmState[r].view + /\ (msg.targetView = 0 \/ msg.targetView = GetNewView(rmState[r].view)) + }) > F + /\ LET pReq == CHOOSE msg \in msgs : msg.type = "PrepareRequest" /\ msg.rm = GetPrimary(rmState[r].view) /\ msg.view = rmState[r].view + IN /\ rmState' = [rmState EXCEPT ![r].type = "cv2"] + /\ msgs' = msgs \cup {[type |-> "ChangeView2", rm |-> r, view |-> rmState[r].view, targetView |-> GetNewView(rmState[r].view), sourceView |-> pReq.sourceView]} + /\ UNCHANGED <> + +\* RMSendChangeView2FromCV2 describes node r sending ChangeView2 message on timeout +\* during waiting for DoCV2 signal from the next primary. +RMSendChangeView2FromCV2(r) == + /\ rmState[r].type = "cv2" + /\ LET cv2s == {msg \in msgs : msg.type = "ChangeView2" /\ msg.view = rmState[r].view} + myCV2s == {msg \in cv2s : msg.rm = r} + myBestCV2 == CHOOSE msg \in myCV2s : \A other \in myCV2s : msg.targetView >= other.targetView + pReq == CHOOSE msg \in msgs : msg.type = "PrepareRequest" /\ msg.rm = GetPrimary(rmState[r].view) /\ msg.view = rmState[r].view + IN /\ Cardinality({msg \in cv2s : msg.targetView = myBestCV2.targetView}) >= M + /\ \neg IsPrimaryInTheView(r, myBestCV2.targetView) + /\ msgs' = msgs \cup {[type |-> "ChangeView2", rm |-> r, view |-> rmState[r].view, targetView |-> GetNewView(myBestCV2.targetView), sourceView |-> pReq.sourceView]} + /\ UNCHANGED <> + +\* RMSendDoCV1ByLeader describes node r that collects enough ChangeView1 messages +\* with target view such that the node r is leader in this view. The leader r +\* broadcasts DoChangeView1 message and the newly-created PrepareRequest message +\* for this view. +RMSendDoCV1ByLeader(r) == + /\ rmState[r].type /= "bad" + /\ rmState[r].type /= "dead" + /\ rmState[r].type /= "blockAccepted" + /\ LET cv1s == {msg \in msgs : msg.type = "ChangeView1" /\ msg.view = rmState[r].view} + followersCV1s == {msg \in cv1s : IsPrimaryInTheView(r, msg.targetView)} \* TODO: this condition won't work starting from N+1 view! + targetView == CHOOSE x \in 1..(MaxView+1) : IsPrimaryInTheView(r, x) + IN /\ Cardinality(followersCV1s) >= M + /\ rmState' = [rmState EXCEPT ![r].type = "prepareSent", ![r].view = targetView] + /\ msgs' = msgs \cup {[type |-> "DoChangeView1", rm |-> r, view |-> rmState[r].view, targetView |-> targetView, sourceView |-> targetView], [type |-> "PrepareRequest", rm |-> r, view |-> targetView, targetView |-> 0, sourceView |-> targetView]} + /\ UNCHANGED <> + +\* RMSendDoCV2ByLeader describes node r that collects enough ChangeView2 messages +\* with target view such that the node r is leader in this view. The leader r +\* broadcasts DoChangeView2 message and the old PrepareRequest message that +\* was migrated from the previous view without changes. +RMSendDoCV2ByLeader(r) == + /\ rmState[r].type /= "bad" + /\ rmState[r].type /= "dead" + /\ rmState[r].type /= "blockAccepted" + /\ LET cv2s == {msg \in msgs : msg.type = "ChangeView2" /\ msg.view = rmState[r].view} + followersCV2s == {msg \in cv2s : IsPrimaryInTheView(r, msg.targetView)} + targetView == CHOOSE x \in 1..(MaxView+1) : IsPrimaryInTheView(r, x) + IN /\ Cardinality(followersCV2s) >= M + /\ LET pReq == CHOOSE msg \in msgs : msg.type = "PrepareRequest" /\ msg.rm = GetPrimary(rmState[r].view) /\ msg.view = rmState[r].view + IN /\ rmState' = [rmState EXCEPT ![r].type = "prepareSent", ![r].view = targetView] + /\ msgs' = msgs \cup {[type |-> "DoChangeView2", rm |-> r, view |-> rmState[r].view, targetView |-> targetView, sourceView |-> pReq.sourceView], [type |-> "PrepareRequest", rm |-> r, view |-> targetView, targetView |-> 0, sourceView |-> pReq.sourceView]} + /\ UNCHANGED <> + +\* RMReceiveDoCV1FromLeader descibes node r that receives DoChangeView1 message from +\* the leader of the target DoCV1's view and changes its view. +RMReceiveDoCV1FromLeader(r) == + /\ rmState[r].type /= "bad" + /\ rmState[r].type /= "blockAccepted" + /\ rmState[r].type /= "dead" + /\ Cardinality({msg \in msgs : msg.type = "DoChangeView1" /\ msg.targetView > rmState[r].view}) /= 0 + /\ LET doCV1s == {msg \in msgs : msg.type = "DoChangeView1" /\ msg.targetView > rmState[r].view} + latestDoCV1 == CHOOSE msg \in doCV1s : \A other \in doCV1s : msg.targetView >= other.targetView + IN /\ rmState' = [rmState EXCEPT ![r].type = "initialized", ![r].view = latestDoCV1.targetView] + /\ UNCHANGED <> + +\* RMReceiveDoCV2FromLeader descibes node r that receives DoChangeView2 message from +\* the leader of the target DoCV2's view and changes its view. +RMReceiveDoCV2FromLeader(r) == + /\ rmState[r].type /= "bad" + /\ rmState[r].type /= "blockAccepted" + /\ rmState[r].type /= "dead" + /\ Cardinality({msg \in msgs : msg.type = "DoChangeView2" /\ msg.targetView > rmState[r].view}) /= 0 + /\ LET doCV2s == {msg \in msgs : msg.type = "DoChangeView2" /\ msg.targetView > rmState[r].view} + latestDoCV2 == CHOOSE msg \in doCV2s : \A other \in doCV2s : msg.targetView >= other.targetView + IN /\ rmState' = [rmState EXCEPT ![r].type = "initialized", ![r].view = latestDoCV2.targetView] + /\ UNCHANGED <> + +\* RMBeBad describes the faulty node r that will send any kind of consensus message starting +\* from the step it's gone wild. This step is enabled only when RMFault is non-empty set. +RMBeBad(r) == + /\ r \in RMFault + /\ Cardinality({rm \in RM : rmState[rm].type = "bad"}) < F + /\ rmState' = [rmState EXCEPT ![r].type = "bad"] + /\ UNCHANGED <> + +\* RMFaultySendCV1 describes sending CV1 message by the faulty node r. To reduce +\* the number of reachable states, the target view of this message is restricted by +\* the next one. +RMFaultySendCV1(r) == + /\ rmState[r].type = "bad" + /\ LET cv == [type |-> "ChangeView1", rm |-> r, view |-> rmState[r].view, targetView |-> GetNewView(rmState[r].view), sourceView |-> rmState[r].view] + IN /\ cv \notin msgs + /\ msgs' = msgs \cup {cv} + /\ UNCHANGED <> + +\* RMFaultySendCV2 describes sending CV2 message by the faulty node r. To reduce +\* the number of reachable states, the target view of this message is restricted by +\* the next one; the source view of this message is restricted by the current one. +RMFaultySendCV2(r) == + /\ rmState[r].type = "bad" + /\ LET cv == [type |-> "ChangeView2", rm |-> r, view |-> rmState[r].view, targetView |-> GetNewView(rmState[r].view), sourceView |-> rmState[r].view] + IN /\ cv \notin msgs + /\ msgs' = msgs \cup {cv} + /\ UNCHANGED <> + +\* RMFaultyDoCV describes view changing by the faulty node r. +RMFaultyDoCV(r) == + /\ rmState[r].type = "bad" + /\ rmState' = [rmState EXCEPT ![r].view = GetNewView(rmState[r].view)] + /\ UNCHANGED <> + +\* RMFaultySendPReq describes sending PrepareRequest message by the primary faulty node r. +\* To reduce the number of reachable states, the sourceView is always restricted by the +\* current r's view. +RMFaultySendPReq(r) == + /\ rmState[r].type = "bad" + /\ IsPrimary(r) + /\ LET pReq == [type |-> "PrepareRequest", rm |-> r, view |-> rmState[r].view, targetView |-> 0, sourceView |-> rmState[r].view] + IN /\ pReq \notin msgs + /\ msgs' = msgs \cup {pReq} + /\ UNCHANGED <> + +\* RMFaultySendPResp describes sending PrepareResponse message by the non-primary faulty node r. +\* To reduce the number of reachable states, the sourceView is always restricted by the +\* current r's view. +RMFaultySendPResp(r) == + /\ rmState[r].type = "bad" + /\ \neg IsPrimary(r) + /\ LET pResp == [type |-> "PrepareResponse", rm |-> r, view |-> rmState[r].view, targetView |-> 0, sourceView |-> rmState[r].view] + IN /\ pResp \notin msgs + /\ msgs' = msgs \cup {pResp} + /\ UNCHANGED <> + +\* RMFaultySendCommit describes sending Commit message by the faulty node r. +\* To reduce the number of reachable states, the sourceView is always restricted by the +\* current r's view. +RMFaultySendCommit(r) == + /\ rmState[r].type = "bad" + /\ LET commit == [type |-> "Commit", rm |-> r, view |-> rmState[r].view, targetView |-> 0, sourceView |-> rmState[r].view] + IN /\ commit \notin msgs + /\ msgs' = msgs \cup {commit} + /\ UNCHANGED <> + +\* We don't describe sending DoCV messages by faulty node, because it can't +\* actually produce other than valid message, and valid message sending is described +\* in the "good" node specification. We also don't describe receiving the DoCV message +\* by the faulty node because it has a separate RMFaultyDoCV action enabled. + +\* RMDie describes node r that was removed from the network at the particular step +\* of the behaviour. After this node r can't change its state and accept/send messages. +RMDie(r) == + /\ r \in RMDead + /\ Cardinality({rm \in RM : rmState[rm].type = "dead"}) < F + /\ rmState' = [rmState EXCEPT ![r].type = "dead"] + /\ UNCHANGED <> + +\* Terminating is an action that allows infinite stuttering to prevent deadlock on +\* behaviour termination. We consider termination to be valid if at least M nodes +\* have the block being accepted. +Terminating == + /\ Cardinality({rm \in RM : rmState[rm].type = "blockAccepted"}) >= M + /\ UNCHANGED vars + + +\* Next is the next-state action describing the transition from the current state +\* to the next state of the behaviour. +Next == + \/ Terminating + \/ \E r \in RM: + RMSendPrepareRequest(r) \/ RMSendPrepareResponse(r) \/ RMSendCommit(r) + \/ RMAcceptBlock(r) + \/ RMSendChangeView1(r) \/ RMSendChangeView1FromCV1(r) + \/ RMSendChangeView2(r) \/ RMSendChangeView2FromCV2(r) + \/ RMSendDoCV1ByLeader(r) \/ RMReceiveDoCV1FromLeader(r) + \/ RMSendDoCV2ByLeader(r) \/ RMReceiveDoCV2FromLeader(r) + \/ RMBeBad(r) + \/ RMFaultySendCV1(r) \/ RMFaultySendCV2(r) \/ RMFaultyDoCV(r) \/ RMFaultySendCommit(r) \/ RMFaultySendPReq(r) \/ RMFaultySendPResp(r) + \/ RMDie(r) \/ RMFetchBlock(r) + +\* Safety is a temporal formula that describes the whole set of allowed +\* behaviours. It specifies only what the system MAY do (i.e. the set of +\* possible allowed behaviours for the system). It asserts only what may +\* happen; any behaviour that violates it does so at some point and +\* nothing past that point makes difference. +\* +\* E.g. this safety formula (applied standalone) allows the behaviour to end +\* with an infinite set of stuttering steps (those steps that DO NOT change +\* neither msgs nor rmState) and never reach the state where at least one +\* node is committed or accepted the block. +\* +\* To forbid such behaviours we must specify what the system MUST +\* do. It will be specified below with the help of fairness conditions in +\* the Fairness formula. +Safety == Init /\ [][Next]_vars + + +\* -------------- Fairness temporal formula -------------- + +\* Fairness is a temporal assumptions under which the model is working. +\* Usually it specifies different kind of assumptions for each/some +\* subactions of the Next's state action, but the only think that bothers +\* us is preventing infinite stuttering at those steps where some of Next's +\* subactions are enabled. Thus, the only thing that we require from the +\* system is to keep take the steps until it's impossible to take them. +\* That's exactly how the weak fairness condition works: if some action +\* remains continuously enabled, it must eventually happen. +Fairness == WF_vars(Next) + +\* -------------- Specification -------------- + +\* The complete specification of the protocol written as a temporal formula. +Spec == Safety /\ Fairness + +\* -------------- Liveness temporal formula -------------- + +\* For every possible behaviour it's true that eventually (i.e. at least once +\* through the behaviour) block will be accepted. It is something that dBFT +\* must guarantee (an in practice this condition is violated). +TerminationRequirement == <>(Cardinality({r \in RM : rmState[r].type = "blockAccepted"}) >= M) + +\* A liveness temporal formula asserts only what must happen (i.e. specifies +\* what the system MUST do). Any behaviour can NOT violate it at ANY point; +\* there's always the rest of the behaviour that can always make the liveness +\* formula true; if there's no such behaviour than the liveness formula is +\* violated. The liveness formula is supposed to be checked as a property +\* by the TLC model checker. +Liveness == TerminationRequirement + +\* -------------- ModelConstraints -------------- + +\* MaxViewConstraint is a state predicate restricting the number of possible +\* behaviour states. It is needed to reduce model checking time and prevent +\* the model graph size explosion. This formulae must be specified at the +\* "State constraint" section of the "Additional Spec Options" section inside +\* the model overview. +MaxViewConstraint == /\ \A r \in RM : rmState[r].view <= MaxView + /\ \A msg \in msgs : msg.targetView = 0 \/ msg.targetView <= MaxView + 1 + +\* -------------- Invariants of the specification -------------- + +\* Model invariant is a state predicate (statement) that must be true for +\* every step of every reachable behaviour. Model invariant is supposed to +\* be checked as an Invariant by the TLC Model Checker. + +\* TypeOK is a type-correctness invariant. It states that all elements of +\* specification variables must have the proper type throughout the behaviour. +TypeOK == + /\ rmState \in [RM -> RMStates] + /\ msgs \subseteq Messages + /\ blockAccepted \in [RM -> Nat] + +\* InvTwoBlocksAcceptedAdvanced ensures that the proposed and accepted block +\* originally comes from the same view for every node that has the block +\* being accepted. +InvTwoBlocksAcceptedAdvanced == \A r1 \in RM: + \A r2 \in RM \ {r1}: + \/ rmState[r1].type /= "blockAccepted" + \/ rmState[r2].type /= "blockAccepted" + \/ blockAccepted[r1] = blockAccepted[r2] + +\* InvFaultNodesCount states that there can be F faulty or dead nodes at max. +InvFaultNodesCount == Cardinality({ + r \in RM : rmState[r].type = "bad" \/ rmState[r].type = "dead" + }) <= F + +\* This theorem asserts the truth of the temporal formula whose meaning is that +\* the state predicates TypeOK, InvTwoBlocksAccepted and InvFaultNodesCount are +\* the invariants of the specification Spec. This theorem is not supposed to be +\* checked by the TLC model checker, it's here for the reader's understanding of +\* the purpose of TypeOK, InvTwoBlocksAccepted and InvFaultNodesCount. +THEOREM Spec => [](TypeOK /\ InvTwoBlocksAcceptedAdvanced /\ InvFaultNodesCount) +============================================================================= +\* Modification History +\* Last modified Fri Mar 03 10:51:05 MSK 2023 by root +\* Last modified Wed Feb 15 15:43:25 MSK 2023 by anna +\* Last modified Mon Jan 23 21:49:06 MSK 2023 by rik +\* Created Thu Dec 15 16:06:17 MSK 2022 by anna \ No newline at end of file diff --git a/formal-models/dbft2.1_centralizedCV/dbftCentralizedCV___AllGoodModel.launch b/formal-models/dbft2.1_centralizedCV/dbftCentralizedCV___AllGoodModel.launch new file mode 100644 index 00000000..64728323 --- /dev/null +++ b/formal-models/dbft2.1_centralizedCV/dbftCentralizedCV___AllGoodModel.launch @@ -0,0 +1,42 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/formal-models/dbft2.1_threeStagedCV/dbftCV3.tla b/formal-models/dbft2.1_threeStagedCV/dbftCV3.tla new file mode 100644 index 00000000..536934ce --- /dev/null +++ b/formal-models/dbft2.1_threeStagedCV/dbftCV3.tla @@ -0,0 +1,427 @@ +-------------------------------- MODULE dbftCV3 -------------------------------- + +EXTENDS + Integers, + FiniteSets + +CONSTANTS + \* RM is the set of consensus node indexes starting from 0. + \* Example: {0, 1, 2, 3} + RM, + + \* RMFault is a set of consensus node indexes that are allowed to become + \* FAULT in the middle of every considered behavior and to send any + \* consensus message afterwards. RMFault must be a subset of RM. An empty + \* set means that all nodes are good in every possible behaviour. + \* Examples: {0} + \* {1, 3} + \* {} + RMFault, + + \* RMDead is a set of consensus node indexes that are allowed to die in the + \* middle of every behaviour and do not send any message afterwards. RMDead + \* must be a subset of RM. An empty set means that all nodes are alive and + \* responding in in every possible behaviour. RMDead may intersect the + \* RMFault set which means that node which is in both RMDead and RMFault + \* may become FAULT and send any message starting from some step of the + \* particular behaviour and may also die in the same behaviour which will + \* prevent it from sending any message. + \* Examples: {0} + \* {3, 2} + \* {} + RMDead, + + \* MaxView is the maximum allowed view to be considered (starting from 0, + \* including the MaxView itself). This constraint was introduced to reduce + \* the number of possible model states to be checked. It is recommended to + \* keep this setting not too high (< N is highly recommended). + \* Example: 2 + MaxView + +VARIABLES + \* rmState is a set of consensus node states. It is represented by the + \* mapping (function) with domain RM and range RMStates. I.e. rmState[r] is + \* the state of the r-th consensus node at the current step. + rmState, + + \* msgs is the shared pool of messages sent to the network by consensus nodes. + \* It is represented by a subset of Messages set. + msgs + +\* vars is a tuple of all variables used in the specification. It is needed to +\* simplify fairness conditions definition. +vars == <> + +\* N is the number of validators. +N == Cardinality(RM) + +\* F is the number of validators that are allowed to be malicious. +F == (N - 1) \div 3 + +\* M is the number of validators that must function correctly. +M == N - F + +\* These assumptions are checked by the TLC model checker once at the start of +\* the model checking process. All the input data (declared constants) specified +\* in the "Model Overview" section must satisfy these constraints. +ASSUME + /\ RM \subseteq Nat + /\ N >= 4 + /\ 0 \in RM + /\ RMFault \subseteq RM + /\ RMDead \subseteq RM + /\ Cardinality(RMFault) <= F + /\ Cardinality(RMDead) <= F + /\ Cardinality(RMFault \cup RMDead) <= F + /\ MaxView \in Nat + /\ MaxView <= 2 + +\* RMStates is a set of records where each record holds the node state and +\* the node current view. +RMStates == [ + type: {"initialized", "prepareSent", "commitSent", "blockAccepted", "cv1", "cv2", "cv3", "bad", "dead"}, + view : Nat + ] + +\* Messages is a set of records where each record holds the message type, +\* the message sender and sender's view by the moment when message was sent. +Messages == [type : {"PrepareRequest", "PrepareResponse", "Commit", "ChangeView1", "ChangeView2", "ChangeView3"}, rm : RM, view : Nat] + +\* -------------- Useful operators -------------- + +\* IsPrimary is an operator defining whether provided node r is primary +\* for the current round from the r's point of view. It is a mapping +\* from RM to the set of {TRUE, FALSE}. +IsPrimary(r) == rmState[r].view % N = r + +\* GetPrimary is an operator defining mapping from round index to the RM that +\* is primary in this round. +GetPrimary(view) == CHOOSE r \in RM : view % N = r + +\* GetNewView returns new view number based on the previous node view value. +\* Current specifications only allows to increment view. +GetNewView(oldView) == oldView + 1 + +\* PrepareRequestSentOrReceived denotes whether there's a PrepareRequest +\* message received from the current round's speaker (as the node r sees it). +PrepareRequestSentOrReceived(r) == [type |-> "PrepareRequest", rm |-> GetPrimary(rmState[r].view), view |-> rmState[r].view] \in msgs + +\* -------------- Safety temporal formula -------------- + +\* Init is the initial predicate initializing values at the start of every +\* behaviour. +Init == + /\ rmState = [r \in RM |-> [type |-> "initialized", view |-> 0]] + /\ msgs = {} + +\* RMSendPrepareRequest describes the primary node r broadcasting PrepareRequest. +RMSendPrepareRequest(r) == + /\ rmState[r].type = "initialized" + /\ IsPrimary(r) + /\ rmState' = [rmState EXCEPT ![r].type = "prepareSent"] + /\ msgs' = msgs \cup {[type |-> "PrepareRequest", rm |-> r, view |-> rmState[r].view]} + /\ UNCHANGED <<>> + +\* RMSendPrepareResponse describes non-primary node r receiving PrepareRequest from +\* the primary node of the current round (view) and broadcasting PrepareResponse. +\* This step assumes that PrepareRequest always contains valid transactions and +\* signatures. +RMSendPrepareResponse(r) == + /\ rmState[r].type = "initialized" + /\ \neg IsPrimary(r) + /\ PrepareRequestSentOrReceived(r) + /\ rmState' = [rmState EXCEPT ![r].type = "prepareSent"] + /\ msgs' = msgs \cup {[type |-> "PrepareResponse", rm |-> r, view |-> rmState[r].view]} + /\ UNCHANGED <<>> + +\* RMSendCommit describes node r sending Commit if there's enough PrepareRequest/PrepareResponse +\* messages and no node has sent the ChangeView3 message. It is possible to send the Commit after +\* the ChangeView1 or ChangeView2 message was sent with additional constraints. +RMSendCommit(r) == + /\ \/ rmState[r].type = "prepareSent" + \/ rmState[r].type = "cv1" + \/ /\ rmState[r].type = "cv2" + /\ Cardinality({ + msg \in msgs : msg.type = "Commit" /\ msg.view = rmState[r].view + }) > F + /\ Cardinality({ + msg \in msgs : (msg.type = "PrepareResponse" \/ msg.type = "PrepareRequest") /\ msg.view = rmState[r].view + }) >= M + /\ Cardinality({ + msg \in msgs : msg.type = "ChangeView3" /\ msg.view = rmState[r].view + }) = 0 + /\ PrepareRequestSentOrReceived(r) + /\ rmState' = [rmState EXCEPT ![r].type = "commitSent"] + /\ msgs' = msgs \cup {[type |-> "Commit", rm |-> r, view |-> rmState[r].view]} + /\ UNCHANGED <<>> + +\* RMAcceptBlock describes node r collecting enough Commit messages and accepting +\* the block. +RMAcceptBlock(r) == + /\ rmState[r].type /= "bad" + /\ rmState[r].type /= "dead" + /\ rmState[r].type /= "blockAccepted" + /\ PrepareRequestSentOrReceived(r) + /\ Cardinality({ + msg \in msgs : msg.type = "Commit" /\ msg.view = rmState[r].view + }) >= M + /\ rmState' = [rmState EXCEPT ![r].type = "blockAccepted"] + /\ UNCHANGED <> + +\* FetchBlock describes node r that fetches the accepted block from some other node. +RMFetchBlock(r) == + /\ rmState[r].type /= "bad" + /\ rmState[r].type /= "dead" + /\ rmState[r].type /= "blockAccepted" + /\ \E rmAccepted \in RM : /\ rmState[rmAccepted].type = "blockAccepted" + /\ rmState' = [rmState EXCEPT ![r].type = "blockAccepted", ![r].view = rmState[rmAccepted].view] + /\ UNCHANGED <> + +\* RMSendChangeView1 describes node r sending ChangeView1 message on timeout. +\* Only non-primary node is allowed to send ChangeView1 message, as the primary +\* must send the PrepareRequest if the timer fires. +RMSendChangeView1(r) == + /\ rmState[r].type = "initialized" + /\ \neg IsPrimary(r) + /\ rmState' = [rmState EXCEPT ![r].type = "cv1"] + /\ msgs' = msgs \cup {[type |-> "ChangeView1", rm |-> r, view |-> rmState[r].view]} + +\* RMSendChangeView2 describes node r sending ChangeView2 message on timeout either from +\* "cv1" state or after the node has sent the PrepareRequest or PrepareResponse message. +RMSendChangeView2(r) == + /\ \/ /\ rmState[r].type = "prepareSent" + /\ Cardinality({ + msg \in msgs : msg.type = "ChangeView1" /\ msg.view = rmState[r].view + }) > 0 + \/ rmState[r].type = "cv1" + /\ Cardinality({ + msg \in msgs : (msg.type = "ChangeView1" \/ msg.type = "PrepareRequest" \/ msg.type = "PrepareResponse") /\ msg.view = rmState[r].view + }) >= M + /\ \/ Cardinality({ + msg \in msgs : msg.type = "Commit" /\ msg.view = rmState[r].view + }) <= F + \/ Cardinality({ + msg \in msgs : msg.type = "ChangeView3" /\ msg.view = rmState[r].view + }) > 0 + /\ rmState' = [rmState EXCEPT ![r].type = "cv2"] + /\ msgs' = msgs \cup {[type |-> "ChangeView2", rm |-> r, view |-> rmState[r].view]} + +\* RMSendChangeView3 describes node r sending ChangeView3 message on timeout either from +\* "cv2" state or after the node has sent the Commit message. +RMSendChangeView3(r) == + /\ \/ rmState[r].type = "cv2" + \/ rmState[r].type = "commitSent" + /\ Cardinality({msg \in msgs : (msg.type = "ChangeView2" \/ msg.type = "Commit") /\ msg.view = rmState[r].view}) >= M + /\ Cardinality({msg \in msgs : (msg.type = "ChangeView2") /\ msg.view = rmState[r].view}) > 0 + /\ Cardinality({msg \in msgs : msg.type = "Commit" /\ msg.view = rmState[r].view}) <= F + /\ rmState' = [rmState EXCEPT ![r].type = "cv3"] + /\ msgs' = msgs \cup {[type |-> "ChangeView3", rm |-> r, view |-> rmState[r].view]} + +\* RMReceiveChangeView describes node r receiving enough ChangeView[1,2,3] messages for +\* view changing. +RMReceiveChangeView(r) == + /\ rmState[r].type /= "bad" + /\ rmState[r].type /= "dead" + /\ rmState[r].type /= "blockAccepted" + /\ \/ Cardinality({rm \in RM : Cardinality({msg \in msgs : /\ msg.rm = rm + /\ msg.type = "ChangeView1" + /\ GetNewView(msg.view) >= GetNewView(rmState[r].view) + }) # 0 + }) >= M + \/ Cardinality({rm \in RM : Cardinality({msg \in msgs : /\ msg.rm = rm + /\ msg.type = "ChangeView2" + /\ GetNewView(msg.view) >= GetNewView(rmState[r].view) + }) # 0 + }) >= M + \/ Cardinality({rm \in RM : Cardinality({msg \in msgs : /\ msg.rm = rm + /\ msg.type = "ChangeView3" + /\ GetNewView(msg.view) >= GetNewView(rmState[r].view) + }) # 0 + }) >= M + /\ rmState' = [rmState EXCEPT ![r].type = "initialized", ![r].view = GetNewView(rmState[r].view)] + /\ UNCHANGED <> + +\* RMBeBad describes the faulty node r that will send any kind of consensus message starting +\* from the step it's gone wild. This step is enabled only when RMFault is non-empty set. +RMBeBad(r) == + /\ r \in RMFault + /\ Cardinality({rm \in RM : rmState[rm].type = "bad"}) < F + /\ rmState' = [rmState EXCEPT ![r].type = "bad"] + /\ UNCHANGED <> + +\* RMFaultySendCV describes sending CV1 message by the faulty node r. +RMFaultySendCV1(r) == + /\ rmState[r].type = "bad" + /\ LET cv == [type |-> "ChangeView1", rm |-> r, view |-> rmState[r].view] + IN /\ cv \notin msgs + /\ msgs' = msgs \cup {cv} + /\ UNCHANGED <> + +\* RMFaultySendCV2 describes sending CV2 message by the faulty node r. +RMFaultySendCV2(r) == + /\ rmState[r].type = "bad" + /\ LET cv == [type |-> "ChangeView2", rm |-> r, view |-> rmState[r].view] + IN /\ cv \notin msgs + /\ msgs' = msgs \cup {cv} + /\ UNCHANGED <> + +\* RMFaultySendCV3 describes sending CV3 message by the faulty node r. +RMFaultySendCV3(r) == + /\ rmState[r].type = "bad" + /\ LET cv == [type |-> "ChangeView3", rm |-> r, view |-> rmState[r].view] + IN /\ cv \notin msgs + /\ msgs' = msgs \cup {cv} + /\ UNCHANGED <> + +\* RMFaultyDoCV describes view changing by the faulty node r. +RMFaultyDoCV(r) == + /\ rmState[r].type = "bad" + /\ rmState' = [rmState EXCEPT ![r].view = GetNewView(rmState[r].view)] + /\ UNCHANGED <> + +\* RMFaultySendPReq describes sending PrepareRequest message by the primary faulty node r. +RMFaultySendPReq(r) == + /\ rmState[r].type = "bad" + /\ IsPrimary(r) + /\ LET pReq == [type |-> "PrepareRequest", rm |-> r, view |-> rmState[r].view] + IN /\ pReq \notin msgs + /\ msgs' = msgs \cup {pReq} + /\ UNCHANGED <> + +\* RMFaultySendPResp describes sending PrepareResponse message by the non-primary faulty node r. +RMFaultySendPResp(r) == + /\ rmState[r].type = "bad" + /\ \neg IsPrimary(r) + /\ LET pResp == [type |-> "PrepareResponse", rm |-> r, view |-> rmState[r].view] + IN /\ pResp \notin msgs + /\ msgs' = msgs \cup {pResp} + /\ UNCHANGED <> + +\* RMFaultySendCommit describes sending Commit message by the faulty node r. +RMFaultySendCommit(r) == + /\ rmState[r].type = "bad" + /\ LET commit == [type |-> "Commit", rm |-> r, view |-> rmState[r].view] + IN /\ commit \notin msgs + /\ msgs' = msgs \cup {commit} + /\ UNCHANGED <> + +\* RMDie describes node r that was removed from the network at the particular step +\* of the behaviour. After this node r can't change its state and accept/send messages. +RMDie(r) == + /\ r \in RMDead + /\ Cardinality({rm \in RM : rmState[rm].type = "dead"}) < F + /\ rmState' = [rmState EXCEPT ![r].type = "dead"] + /\ UNCHANGED <> + +\* Terminating is an action that allows infinite stuttering to prevent deadlock on +\* behaviour termination. We consider termination to be valid if at least M nodes +\* has the block being accepted. +Terminating == + /\ Cardinality({rm \in RM : rmState[rm].type = "blockAccepted"}) >= M + /\ UNCHANGED <> + +\* The next-state action. +Next == + \/ Terminating + \/ \E r \in RM: + RMSendPrepareRequest(r) \/ RMSendPrepareResponse(r) \/ RMSendCommit(r) + \/ RMAcceptBlock(r) \/ RMSendChangeView1(r) \/ RMReceiveChangeView(r) \/ RMBeBad(r) \/ RMSendChangeView2(r) \/ RMSendChangeView3(r) + \/ RMFaultySendCV1(r) \/ RMFaultyDoCV(r) \/ RMFaultySendCommit(r) \/ RMFaultySendPReq(r) \/ RMFaultySendPResp(r) \/ RMFaultySendCV2(r) \/ RMFaultySendCV3(r) + \/ RMDie(r) \/ RMFetchBlock(r) + +\* Safety is a temporal formula that describes the whole set of allowed +\* behaviours. It specifies only what the system MAY do (i.e. the set of +\* possible allowed behaviours for the system). It asserts only what may +\* happen; any behaviour that violates it does so at some point and +\* nothing past that point makes difference. +\* +\* E.g. this safety formula (applied standalone) allows the behaviour to end +\* with an infinite set of stuttering steps (those steps that DO NOT change +\* neither msgs nor rmState) and never reach the state where at least one +\* node is committed or accepted the block. +\* +\* To forbid such behaviours we must specify what the system MUST +\* do. It will be specified below with the help of fairness conditions in +\* the Fairness formula. +Safety == Init /\ [][Next]_vars + +\* -------------- Fairness temporal formula -------------- + +\* Fairness is a temporal assumptions under which the model is working. +\* Usually it specifies different kind of assumptions for each/some +\* subactions of the Next's state action, but the only think that bothers +\* us is preventing infinite stuttering at those steps where some of Next's +\* subactions are enabled. Thus, the only thing that we require from the +\* system is to keep take the steps until it's impossible to take them. +\* That's exactly how the weak fairness condition works: if some action +\* remains continuously enabled, it must eventually happen. +Fairness == WF_vars(Next) + +\* -------------- Specification -------------- + +\* The complete specification of the protocol written as a temporal formula. +Spec == Safety /\ Fairness + +\* -------------- Liveness temporal formula -------------- + +\* For every possible behaviour it's true that eventually (i.e. at least once +\* through the behaviour) block will be accepted. It is something that dBFT +\* must guarantee (an in practice this condition is violated). +TerminationRequirement == <>(Cardinality({r \in RM : rmState[r].type = "blockAccepted"}) >= M) + +\* A liveness temporal formula asserts only what must happen (i.e. specifies +\* what the system MUST do). Any behaviour can NOT violate it at ANY point; +\* there's always the rest of the behaviour that can always make the liveness +\* formula true; if there's no such behaviour than the liveness formula is +\* violated. The liveness formula is supposed to be checked as a property +\* by the TLC model checker. +Liveness == TerminationRequirement + +\* -------------- ModelConstraints -------------- + +\* MaxViewConstraint is a state predicate restricting the number of possible +\* behaviour states. It is needed to reduce model checking time and prevent +\* the model graph size explosion. This formulae must be specified at the +\* "State constraint" section of the "Additional Spec Options" section inside +\* the model overview. +MaxViewConstraint == /\ \A r \in RM : rmState[r].view <= MaxView + /\ \A msg \in msgs : msg.view <= MaxView + +\* -------------- Invariants of the specification -------------- + +\* Model invariant is a state predicate (statement) that must be true for +\* every step of every reachable behaviour. Model invariant is supposed to +\* be checked as an Invariant by the TLC Model Checker. + +\* TypeOK is a type-correctness invariant. It states that all elements of +\* specification variables must have the proper type throughout the behaviour. +TypeOK == + /\ rmState \in [RM -> RMStates] + /\ msgs \subseteq Messages + +\* InvTwoBlocksAccepted states that there can't be two different blocks accepted in +\* the two different views, i.e. dBFT must not allow forks. +InvTwoBlocksAccepted == \A r1 \in RM: + \A r2 \in RM \ {r1}: + \/ rmState[r1].type /= "blockAccepted" + \/ rmState[r2].type /= "blockAccepted" + \/ rmState[r1].view = rmState[r2].view + +\* InvFaultNodesCount states that there can be F faulty or dead nodes at max. +InvFaultNodesCount == Cardinality({ + r \in RM : rmState[r].type = "bad" \/ rmState[r].type = "dead" + }) <= F + +\* This theorem asserts the truth of the temporal formula whose meaning is that +\* the state predicates TypeOK, InvTwoBlocksAccepted and InvFaultNodesCount are +\* the invariants of the specification Spec. This theorem is not supposed to be +\* checked by the TLC model checker, it's here for the reader's understanding of +\* the purpose of TypeOK, InvTwoBlocksAccepted and InvFaultNodesCount. +THEOREM Spec => [](TypeOK /\ InvTwoBlocksAccepted /\ InvFaultNodesCount) + +============================================================================= +\* Modification History +\* Last modified Wed Mar 01 12:11:07 MSK 2023 by root +\* Last modified Tue Feb 07 23:11:19 MSK 2023 by rik +\* Last modified Fri Feb 03 18:09:33 MSK 2023 by anna +\* Created Thu Dec 15 16:06:17 MSK 2022 by anna diff --git a/formal-models/dbft2.1_threeStagedCV/dbftCV3___AllGoodModel.launch b/formal-models/dbft2.1_threeStagedCV/dbftCV3___AllGoodModel.launch new file mode 100644 index 00000000..db8b3ead --- /dev/null +++ b/formal-models/dbft2.1_threeStagedCV/dbftCV3___AllGoodModel.launch @@ -0,0 +1,42 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +