{"id":342805,"date":"2021-02-13T22:05:52","date_gmt":"2021-02-13T14:05:52","guid":{"rendered":"http:\/\/4563.org\/?p=342805"},"modified":"2021-02-13T22:05:52","modified_gmt":"2021-02-13T14:05:52","slug":"%e6%80%8e%e4%b9%88%e7%90%86%e8%a7%a3%e5%b9%b6%e5%8f%91%e7%bc%96%e7%a8%8b%e4%b8%ad%e7%9a%84-invirants%ef%bc%9f","status":"publish","type":"post","link":"http:\/\/4563.org\/?p=342805","title":{"rendered":"\u600e\u4e48\u7406\u89e3\u5e76\u53d1\u7f16\u7a0b\u4e2d\u7684 invirants\uff1f"},"content":{"rendered":"
\n
\n
\n

\u600e\u4e48\u7406\u89e3\u5e76\u53d1\u7f16\u7a0b\u4e2d\u7684 invirants\uff1f <\/h1>\n

<\/p>\n

\n
\u8cc7\u6df1\u5927\u4f6c : RedBlackTree <\/span> <\/i> 3<\/span> <\/div>\n
<\/div>\n<\/p><\/div>\n<\/p><\/div>\n<\/p><\/div>\n
<\/p>\n

\u770b GOPl \u90a3\u672c\u84dd\u76ae\u4e66\u65f6\uff0c\u7b2c\u4e5d\u7ae0\u8bb2\u5171\u4eab\u53d8\u91cf\uff0c\u5176\u4e2d\u8bb2\u5230 sync.Mutex \u662f\u4e0d\u53ef\u91cd\u5165\u7684\uff0c\u5df2\u7ecf\u83b7\u5f97 Lock \u7684 goroutine \u91cd\u590d\u8c03\u7528 Lock\uff0c\u4e5f\u4f1a\u963b\u585e\u3002\u7136\u540e 9.2 \u8282\uff08\u82f1\u6587\u7248 265 \u9875\uff09\u6709\u4e0b\u9762\u8fd9\u6bb5\u8bdd\uff1a<\/p>\n

\n

There is a good reason Go’s mutexes are not re-entrant. The purpose of a mutex is to ensure that certain invariants of the shared variables are maintained at critical points during program execution. One of the invariants is “no goroutine is accessing the shared variables”, but there may be additional invariants specific to the data structures that the mutex guards. When a goroutine acquires a mutex lock, it may assume that the invirants hold. While it holds the lock, it may update the shared variables so that the invariants are temporarily violated. However, when it releases the lock, it must guarantee that the order has been restored and the invariants hold once again. Although a re-entrant mutex would ensure that no other goroutines are accessing the shared variables, it cannot protect the additional invariants of those variables.<\/p>\n<\/blockquote>\n

\u8bfb\u4e86\u5f88\u591a\u904d\u8fd8\u662f\u89c9\u5f97\u96be\u4ee5\u7406\u89e3\uff0cinvariants \u5e94\u8be5\u662f\u67d0\u4e9b\u4e0d\u53d8\u7684\u5c5e\u6027\uff0c\u4e0d\u53d8\u91cf\u7684\u610f\u601d\uff0c\u4f46\u662f\u539f\u6587\u6240\u8bf4\u7684\u9664\u4e86\u201c\u6ca1\u6709\u5176\u4ed6 goroutine \u8bbf\u95ee\u8fd9\u4e2a\u53d8\u91cf\u201d\u8fd9\u4e2a invariant \u4e4b\u5916\uff0cmutex \u4fdd\u62a4\u7684\u8fd8\u6709\u522b\u7684 invariant \u3002\u5177\u4f53\u662f\u6307\u4ec0\u4e48\u6709\u524d\u8f88\u6307\u70b9\u4e0b\uff1f<\/p>\n<\/p><\/div>\n

\u5927\u4f6c\u6709\u8a71\u8aaa<\/b> (8<\/span>) <\/div>\n
<\/div>\n<\/p><\/div>\n<\/p><\/div>\n
    \n
  • \n
    \n
    \n
    \u4e3b<\/span> \u8cc7\u6df1\u5927\u4f6c : RedBlackTree <\/span> <\/div>\n
    <\/i> <\/span> <\/div>\n<\/p><\/div>\n
    \u8865\u5145\u4e00\u4e0b\uff0c\u5728 MIT6.824 \u5206\u5e03\u5f0f\u7cfb\u7edf\u90a3\u95e8\u8bfe\uff0c\u6709\u4e00\u8282\u8bfe\u90a3\u4e2a\u5370\u5ea6\u52a9\u6559\u5728\u8bb2\u9501\u65f6\u4e5f\u63d0\u5230\u8fc7 invariants\uff0c\u4ed6\u8bf4\u7684\u662f\uff1a\u201cmutex \u4e0d\u662f\u7528\u6765\u4fdd\u62a4\u53d8\u91cf\u7684\uff0c\u800c\u662f\u7528\u6765\u4fdd\u62a4 invariants \u7684\uff0c\u9664\u4e86\u53ea\u6709\u4e00\u4e2a goroutine \u8bbf\u95ee\u8fd9\u4e2a\u53d8\u91cf\uff0c\u8fd8\u6709\u5176\u4ed6\u7684 invariants\u201d\uff0c\u5927\u6982\u8fd9\u4e2a\u610f\u601d\u3002\u6211\u4f30\u8ba1\u4ed6\u4e5f\u662f\u8bfb\u4e86\u8fd9\u672c\u4e66\uff0c\u8ddf\u4e66\u4e0a\u7684\u8bf4\u6cd5\u57fa\u672c\u4e00\u81f4\uff0c\u4f46\u662f\u4ed6\u4e5f\u6ca1\u6709\u518d\u8be6\u7ec6\u89e3\u91ca\u3002 <\/div>\n<\/p><\/div>\n<\/li>\n
  • \n
    \n
    \n
    \u8cc7\u6df1\u5927\u4f6c : hxndg <\/span> <\/div>\n
    <\/i> <\/span> <\/div>\n<\/p><\/div>\n
    invariants \u503c\u5f97\u5e94\u8be5\u662f\u4e0d\u53d8\u5f0f\uff0c\u591a\u7ebf\u7a0b\u73af\u5883\u4e0b\uff0c
    \u9501\u4fdd\u62a4\u7684\u4e0d\u53d8\u5f0f\u5e94\u8be5\u662f\u4e24\u4e2a\uff1a
    1 no share thread connect
    2 sequency consistent<\/p>\n

    \u611f\u89c9\u8fd9\u91cc\u7684\u610f\u601d\u8bf4\u7684\u5e94\u8be5\u662f\u7b2c\u4e8c\u4e2a\u3002\u4e0d\u8fc7\u8fd9\u4e2a\u90fd\u662f\u8ddf\u5185\u5b58\u6a21\u578b\u6709\u5173\u7684\uff0c\u6211\u53ea\u80fd\u60f3\u5230\u8fd9\u4e2a\u3002
    \u4f60\u53bb stackoverflow \u641c\u4e00\u4e0b lock invariants \u5e94\u8be5\u6709\u76f8\u5173\u7684\u3002 <\/div>\n<\/p><\/div>\n<\/li>\n

  • \n
    \n
    \n
    \u8cc7\u6df1\u5927\u4f6c : geelaw <\/span> <\/div>\n
    <\/i> <\/span> <\/div>\n<\/p><\/div>\n
    Invariant \u7684\u610f\u601d\u548c\u5e76\u884c\u3001\u5e76\u53d1\u5173\u7cfb\u4e0d\u5927\u3002\u4e0d\u53d8\u91cf\u5c31\u662f\u8bf4\u201c\u6570\u636e\u7684\u7ec4\u7ec7\u5f62\u5f0f\u7b26\u5408\u8be5\u6570\u636e\u7ed3\u6784\u7684\u8981\u6c42\u201d\uff0c\u6bd4\u5982\u4e00\u4e2a\u53cc\u5411\u94fe\u8868\u91cc\u4efb\u4f55\u975e\u5c3e\u8282\u70b9 x \u90fd\u6709 x.next.prev \u7b49\u4e8e x \u4e14\u4efb\u4f55\u975e\u5934\u8282\u70b9 x \u90fd\u6709 x.prev.next \u7b49\u4e8e x \u3002<\/p>\n

    \u5f53\u7f16\u8f91\u94fe\u8868\u65f6\uff0c\u8981\u5bf9\u591a\u4e2a\u5bf9\u8c61\u7684 prev \u3001next \u5206\u522b\u91cd\u65b0\u8d4b\u503c\uff0c\u51e0\u4e2a\u8d4b\u503c\u64cd\u4f5c\u4e4b\u95f4\u7684\u65f6\u523b\uff0c\u4e0d\u6ee1\u8db3\u4e0d\u53d8\u91cf\u3002\u7f16\u8f91\u64cd\u4f5c\u4fdd\u8bc1\uff1a\u64cd\u4f5c\u524d\u7b26\u5408\u4e0d\u53d8\u91cf\uff0c\u5219\u64cd\u4f5c\u5b8c\u6210\u540e\u8fd8\u662f\u7b26\u5408\u3002<\/p>\n

    \u5982\u679c\u94fe\u8868\u88ab\u5e76\u884c\u4fee\u6539\u5219\u53ef\u80fd\u51fa\u95ee\u9898\uff0c\u8fd9\u662f\u56e0\u4e3a\u6709\u7684\u65f6\u5019\uff0c\u7f16\u8f91\u5f00\u59cb\u7684\u65f6\u5019\u94fe\u8868\u4e0d\u6ee1\u8db3\u5b83\u7684\u4e0d\u53d8\u91cf\uff08\u4f8b\u5982\u53e6\u4e00\u4e2a\u4eba\u4e5f\u5728\u7f16\u8f91\u5b83\uff09\u3002\u4e8e\u662f\u4f60\u53ef\u4ee5\u7528\u4e00\u4e2a mutex \u4fdd\u62a4\u94fe\u8868\uff0c\u8bbe\u539f\u5148\u7684\u4e0d\u53d8\u91cf\u662f\u547d\u9898 P\uff0c\u5219\u65b0\u7684\u4e0d\u53d8\u91cf\u6539\u6210\uff1a\u5f53 mutex \u672a\u9501\u5b9a\u65f6\uff0cP \u6210\u7acb\u3002<\/p>\n

    \u5982\u679c mutex \u4e0d\u53ef\u91cd\u5165\uff0c\u5219\u4e0a\u8ff0\u547d\u9898\u7684\u7b80\u5355\u63a8\u8bba\u662f\uff1a\u5f53 mutex \u521a\u88ab\u83b7\u53d6\u65f6\uff0cP \u6210\u7acb\u3002
    \u5982\u679c mutex \u53ef\u91cd\u5165\uff0c\u5219\u4e0a\u8ff0\u63a8\u8bba\u4e0d\u6210\u7acb\uff0c\u56e0\u4e3a\u91cd\u5165\u65f6 P \u4e0d\u4e00\u5b9a\u6210\u7acb\u3002<\/p>\n

    \u90a3\u6bb5\u6559\u7a0b\u5c31\u662f\u5728\u8bf4\uff0c\u5927\u5bb6\u90fd\u5e0c\u671b\u8be5\u63a8\u8bba\u6210\u7acb\uff08\u4ece\u800c\u9a8c\u8bc1\u6b63\u786e\u6027\u4f1a\u66f4\u7b80\u5355\uff09\uff0c\u6240\u4ee5\u6211\u4eec\u8bbe\u8ba1\u7684 mutex \u4e0d\u53ef\u91cd\u5165\u3002 <\/p><\/div>\n<\/p><\/div>\n<\/li>\n

  • \n
    \n
    \n
    \u8cc7\u6df1\u5927\u4f6c : momocraft <\/span> <\/div>\n
    <\/i> <\/span> <\/div>\n<\/p><\/div>\n
    \u4e00\u4e2a\u6570\u636e\u7ed3\u6784\u7684\uff08\u65e0\u6cd5\u76f4\u63a5\u7528\u7f16\u7a0b\u8bed\u8a00\u4fdd\u8bc1\u7684\uff09\u7ea6\u5b9a
    \u6bd4\u5982\u6709\u4e24\u4e2a mutable field\uff0c\u4e00\u4e2a a \u4e00\u4e2a b\uff0c\u8981\u6c42 b \u662f a \u7684\u9636\u4e58\uff08”invariant”\uff09<\/p>\n

    \u66f4\u65b0\u8fd9\u4e24\u4e2a field \u7684\u7ebf\u7a0b\u4e0d\u53ef\u80fd\u540c\u65f6\u5199 a \u548c b\uff0c\u4f46\u53ef\u4ee5\u7528\u4e00\u4e2a mutex \u9650\u5236\u522b\u7684\u7ebf\u7a0b\u770b\u5230
    \u53ea\u8981\u8bfb\u5199\u90fd\u53d1\u751f\u5728\u7ebf\u7a0b\u62ff\u5230 mutex lock \u65f6\uff0c\u5c31\u4e0d\u4f1a\u89c2\u6d4b\u5230\u4e0d\u4e00\u81f4 <\/div>\n<\/p><\/div>\n<\/li>\n

  • \n
    \n
    \n
    \u8cc7\u6df1\u5927\u4f6c : carlclone <\/span> <\/div>\n
    <\/i> <\/span> <\/div>\n<\/p><\/div>\n
    \u4e0d\u662f\u4e0d\u53d8\u91cf\uff0c\u662f\u4e0d\u53d8\u5f0f\uff0c\u6211\u89c9\u5f97\u8fd8\u662f\u4e0d\u8981\u88ab\u8fd9\u4e9b\u7406\u8bba\u7684\u4e1c\u897f\u56f0\u592a\u4e45\u4e86,\u76f4\u63a5\u505a lab \u8fdf\u65e9\u4f1a\u9047\u5230\u7684 <\/div>\n<\/p><\/div>\n<\/li>\n
  • \n
    \n
    \n
    \u8cc7\u6df1\u5927\u4f6c : lance6716 <\/span> <\/div>\n
    <\/i> <\/span> <\/div>\n<\/p><\/div>\n
    \u4e3e\u4e2a\u4f8b\u5b50\uff0c\u5047\u8bbe\u6709\u4e00\u4e2a\u4e0d\u53d8\u91cf\uff0ca+b=10 \u3002\u6709\u4e2a\u64cd\u4f5c\u662f a:=b\uff0cb:=a \u3002<\/p>\n

    \u5728\u5355\u7ebf\u7a0b\u7684\u65f6\u5019\uff0c\u8fd9\u4e2a\u64cd\u4f5c\u524d\u3001\u540e\u90fd\u6ee1\u8db3\u4e0d\u53d8\u91cf\uff0c\u5728\u64cd\u4f5c\u4e2d\u6709\u77ed\u6682\u7684\u4e0d\u6ee1\u8db3\u3002<\/p>\n

    \u5728\u591a\u7ebf\u7a0b\u7684\u65f6\u5019\uff0c\u5982\u679c\u64cd\u4f5c\u4e2d\u53d1\u751f\u4e86\u8c03\u5ea6\uff0c\u5c31\u4e0d\u80fd\u4fdd\u8bc1\u201c\u64cd\u4f5c\u540e\u8fd8\u6ee1\u8db3\u4e0d\u53d8\u91cf\u4e86\u201d\u3002\u5728\u8fd9\u4e2a\u610f\u4e49\u4e0a\uff0c\u9501\u662f\u5728\u4fdd\u62a4\u4e0d\u53d8\u91cf\uff0c\u5c06\u5176\u53d8\u6210\u4e00\u4e2a\u5355\u7ebf\u7a0b\u573a\u666f\u3002\u4e5f\u5c31\u662f\u9501\u7684\u4fdd\u62a4\u8303\u56f4\u4e0b\uff0c\u5c31\u662f\u90a3\u4e2a\u201c\u77ed\u6682\u7684\u4e0d\u6ee1\u8db3\u201d\uff0c\u79bb\u5f00\u8fd9\u4e2a\u8303\u56f4\uff0c\u7ef4\u62a4\u597d\u4e86\u4e0d\u53d8\u91cf\u3002<\/p>\n

    \u91cd\u5165\u9501\u662f\u4e0d\u80fd\u4fdd\u62a4\u4e0d\u53d8\u91cf\u7684\u3002\u4e3e\u4e2a\u590d\u6742\u4e00\u70b9\u7684\u4f8b\u5b50\uff0c\u64cd\u4f5c\u662f t:=a\uff0ca:=b\uff0cb:=t \u3002\u5982\u679c\u5728 a:=b\uff0cb:=t \u4e4b\u95f4\u53d1\u751f\u8c03\u5ea6\u91cd\u5165\u7684\u8bdd\uff0c\u539f\u59cb a \u7684\u503c\u5c31\u4e22\u5931\u4e86\uff0c\u4e5f\u5c31\u4e0d\u80fd\u6ee1\u8db3\u4e0d\u53d8\u91cf\u4e86\u3002 <\/p><\/div>\n<\/p><\/div>\n<\/li>\n

  • \n
    \n
    \n
    \u8cc7\u6df1\u5927\u4f6c : lance6716 <\/span> <\/div>\n
    <\/i> <\/span> <\/div>\n<\/p><\/div>\n
    6 \u5e94\u8be5\u4e24\u4e2a\u64cd\u4f5c\u90fd\u662f\u201ct:=a\uff0ca:=b\uff0cb:=t\u201d <\/div>\n<\/p><\/div>\n<\/li>\n
  • \n
    \n
    \n
    \u4e3b<\/span> \u8cc7\u6df1\u5927\u4f6c : RedBlackTree <\/span> <\/div>\n
    <\/i> <\/span> <\/div>\n<\/p><\/div>\n
    @geelaw \u7406\u89e3\u4e86\uff0c\u975e\u5e38\u611f\u8c22 <\/div>\n<\/p><\/div>\n<\/li>\n
  • \n","protected":false},"excerpt":{"rendered":"

    \u600e\u4e48\u7406\u89e3\u5e76\u53d1\u7f16\u7a0b\u4e2d\u7684 invira…<\/p>\n","protected":false},"author":1,"featured_media":0,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":[],"categories":[],"tags":[],"_links":{"self":[{"href":"http:\/\/4563.org\/index.php?rest_route=\/wp\/v2\/posts\/342805"}],"collection":[{"href":"http:\/\/4563.org\/index.php?rest_route=\/wp\/v2\/posts"}],"about":[{"href":"http:\/\/4563.org\/index.php?rest_route=\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"http:\/\/4563.org\/index.php?rest_route=\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"http:\/\/4563.org\/index.php?rest_route=%2Fwp%2Fv2%2Fcomments&post=342805"}],"version-history":[{"count":0,"href":"http:\/\/4563.org\/index.php?rest_route=\/wp\/v2\/posts\/342805\/revisions"}],"wp:attachment":[{"href":"http:\/\/4563.org\/index.php?rest_route=%2Fwp%2Fv2%2Fmedia&parent=342805"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"http:\/\/4563.org\/index.php?rest_route=%2Fwp%2Fv2%2Fcategories&post=342805"},{"taxonomy":"post_tag","embeddable":true,"href":"http:\/\/4563.org\/index.php?rest_route=%2Fwp%2Fv2%2Ftags&post=342805"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}