tag:blogger.com,1999:blog-410416665291724878.post6571984070501356883..comments2022-12-19T13:52:22.907+04:00Comments on >рабочие заметки: Квест по внутренностям JMM: solutionRuslan Chereminhttp://www.blogger.com/profile/01023948540752159657noreply@blogger.comBlogger41125tag:blogger.com,1999:blog-410416665291724878.post-50228470014034682332013-11-27T17:52:05.538+04:002013-11-27T17:52:05.538+04:00Только судя по обсуждению там в доказательства так...Только судя по обсуждению там в доказательства такая же ошибкаAndreyhttps://www.blogger.com/profile/00631833282868227233noreply@blogger.comtag:blogger.com,1999:blog-410416665291724878.post-13406162938313620112013-11-27T17:10:00.332+04:002013-11-27T17:10:00.332+04:00Доказательство через comittment procedure от Алекс...Доказательство через comittment procedure от Алексея Шипилева читаем на concurrency interestAndreyhttps://www.blogger.com/profile/00631833282868227233noreply@blogger.comtag:blogger.com,1999:blog-410416665291724878.post-41570533722673997682013-11-25T23:42:01.770+04:002013-11-25T23:42:01.770+04:00А я тоже перечитывал с месяц-полтора назад и смути...А я тоже перечитывал с месяц-полтора назад и смутился. Но как-то застремался отрепортить.gvsmirnovhttps://www.blogger.com/profile/09213176675225121755noreply@blogger.comtag:blogger.com,1999:blog-410416665291724878.post-64043069083145560922013-11-25T21:09:31.194+04:002013-11-25T21:09:31.194+04:00Ну во-первых пост писался в ходе подготовки к докл...Ну во-первых пост писался в ходе подготовки к докладу про JMM -- и цель была в том числе понять, насколько люди вообще понимают модель рассуждений, которую предлагает JMM. И когда я обнаружил ошибку, то решил оставить как есть -- насколько быстро кто-нибудь найдет ошибку? Вы, собственно, первый. <br /><br />А во-вторых -- ну неловко было, конечно, так громко размотать, а потом облажаться. Ruslan Chereminhttps://www.blogger.com/profile/01023948540752159657noreply@blogger.comtag:blogger.com,1999:blog-410416665291724878.post-19236228121374661582013-11-25T14:00:16.386+04:002013-11-25T14:00:16.386+04:00Руслан, а Вы не написали в комментариях про ошибоч...Руслан, а Вы не написали в комментариях про ошибочность доказательства, чтобы развлечь читатателей вашего блога?:)Andreyhttps://www.blogger.com/profile/00631833282868227233noreply@blogger.comtag:blogger.com,1999:blog-410416665291724878.post-21599122238780933282013-11-19T23:36:40.075+04:002013-11-19T23:36:40.075+04:00Ага, доказательство ошибочно. То, что 6 so 2 не до...Ага, доказательство ошибочно. То, что 6 so 2 не допускает быть 3 hb 5, но вполне позволяет 3 и 5 быть никак не упорядоченными по hb. И поэтому не мешает 5 прочитать результат 3, хотя бы и "против" so.<br /><br />Поскольку код очевидно содержит data race, то его надо анализировать анализировать с позиций "большой" модели памяти, с commitment procedure и сопутствующим адом. Я Ruslan Chereminhttps://www.blogger.com/profile/01023948540752159657noreply@blogger.comtag:blogger.com,1999:blog-410416665291724878.post-72844830361402356792013-11-17T03:58:25.473+04:002013-11-17T03:58:25.473+04:00Точнее будет отношение SO, но не SWТочнее будет отношение SO, но не SWAndreyhttps://www.blogger.com/profile/00631833282868227233noreply@blogger.comtag:blogger.com,1999:blog-410416665291724878.post-54966583659558823352013-11-17T03:53:53.980+04:002013-11-17T03:53:53.980+04:00Замечание 2:
Synchronized actions (к которым п...Замечание 2:<br /> Synchronized actions (к которым принадлежат vstore и vload) образуют total synchronization order, SO. Важно здесь, что это именно полный порядок. То есть для любых двух SA1, SA2 всегда либо SA1 so SA2, либо SA2 so SA1.<br /><br />Это верно<br /><br />Поскольку (2) и (6) — synchronized actions, то из ![ (2) sw (6) ] => [(6) sw (2) ] => [(6) hb (2)]. Это ключевой, самый Andreyhttps://www.blogger.com/profile/00631833282868227233noreply@blogger.comtag:blogger.com,1999:blog-410416665291724878.post-23583621943068431132013-09-26T09:32:53.301+04:002013-09-26T09:32:53.301+04:00sw == synchronized-withsw == synchronized-withRuslan Chereminhttps://www.blogger.com/profile/01023948540752159657noreply@blogger.comtag:blogger.com,1999:blog-410416665291724878.post-85067925885628916102013-09-24T17:37:01.151+04:002013-09-24T17:37:01.151+04:00Экскьюзмуа,
hb - это happens before, а что такое ...Экскьюзмуа, <br />hb - это happens before, а что такое sw?Anonymousnoreply@blogger.comtag:blogger.com,1999:blog-410416665291724878.post-4223868158252710662013-02-26T14:15:00.755+04:002013-02-26T14:15:00.755+04:00Roach motelRoach motelAnonymoushttps://www.blogger.com/profile/04714052384955388796noreply@blogger.comtag:blogger.com,1999:blog-410416665291724878.post-22188758454549076132013-02-26T11:32:25.543+04:002013-02-26T11:32:25.543+04:00Злой ты :(Злой ты :(gvsmirnovhttps://www.blogger.com/profile/09213176675225121755noreply@blogger.comtag:blogger.com,1999:blog-410416665291724878.post-81106264297617827322013-02-25T20:39:56.073+04:002013-02-25T20:39:56.073+04:00Apache tomcat? Ты, наверное, хотел сказать Apache ...Apache tomcat? Ты, наверное, хотел сказать Apache mod_perl? ;)Ruslan Chereminhttps://www.blogger.com/profile/01023948540752159657noreply@blogger.comtag:blogger.com,1999:blog-410416665291724878.post-52458199839477267252013-02-25T17:48:35.260+04:002013-02-25T17:48:35.260+04:00Но подожди, разве субатомарное частичное отношение...Но подожди, разве субатомарное частичное отношение между hb 2 3 не приводит к сбросу кешей?<br /><br />Вот выдержка из документации по Apache Tomcat (http://clck.ru/846):<br /><br />> Given a Write W, and a Read R, such that R ha W, a Freeze F and a Synchronization Strategy S,<br />> such that S fml F, it is safe to assume that the caches will be flushed after F. JMM also guarantees that<brgvsmirnovhttps://www.blogger.com/profile/09213176675225121755noreply@blogger.comtag:blogger.com,1999:blog-410416665291724878.post-41026573141557992902013-02-22T23:27:00.507+04:002013-02-22T23:27:00.507+04:00Если вы еще раз внимательно прочитаете пункт 7, то...Если вы еще раз внимательно прочитаете пункт 7, то вы сможете увидеть, что этот пункт как раз и показывает, каким образом два потока начинают share happens-before relationship. А именно: их частичные порядки сливаются ("замыкаются") через свойство транзитивности соотношения HB, с помощью того факта, что [(6) hb (2)]. <br /><br />У абсолютного большинства программистов в голове из JMM Ruslan Chereminhttps://www.blogger.com/profile/01023948540752159657noreply@blogger.comtag:blogger.com,1999:blog-410416665291724878.post-1990662800536435602013-02-22T23:03:50.203+04:002013-02-22T23:03:50.203+04:00(из JLS)
...More specifically, if two actions shar...(из JLS)<br />...More specifically, if two actions share a happens-before relationship, they do not<br />necessarily have to appear to have happened in that order to any code with which<br />they do not share a happens-before relationship. Writes in one thread that are in<br />a data race with reads in another thread may, for example, appear to occur out of<br />order to those reads.<br /><br />rxhttps://www.blogger.com/profile/09629498229082478535noreply@blogger.comtag:blogger.com,1999:blog-410416665291724878.post-18086499555092467482013-02-15T14:03:59.205+04:002013-02-15T14:03:59.205+04:00Соплей много как раз потому, что такая перестановк...Соплей много как раз потому, что такая перестановка чаще всего таки возможна. Если вы уберете volatile с value -- она станет возможна. Даже если вы оставите volatile, но добавите в класс других полей -- все станет не так просто. Если value будет меняться несколько раз -- все опять же будет не так просто...Ruslan Chereminhttps://www.blogger.com/profile/01023948540752159657noreply@blogger.comtag:blogger.com,1999:blog-410416665291724878.post-30998342559630878332013-02-15T13:59:06.575+04:002013-02-15T13:59:06.575+04:00@andrey
Частью на ваши вопросы можно ответить. Мо...@andrey<br /><br />Частью на ваши вопросы можно ответить. Модель памяти оперирует действиями с памятью (сюрприз!). Более конкретно -- с разделяемой памятью, т.е локальные переменные и параметры методов ей не интересны. В рамках модели есть "действия с (разделяемой) памятью", есть некоторые "внешние действия" (external action), типа ввода-вывода, и есть синтетические действия, Ruslan Chereminhttps://www.blogger.com/profile/01023948540752159657noreply@blogger.comtag:blogger.com,1999:blog-410416665291724878.post-38898252038163528532013-02-15T13:48:59.610+04:002013-02-15T13:48:59.610+04:00@Ruslan
Я ничего не говорил про зависимые по данны...@Ruslan<br />Я ничего не говорил про зависимые по данным инструкции<br /><br />Интересно, что тут http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.112.1790&rep=rep1&type=pdf<br />утверждается, что перестановка независимых инструкций в текущем виде JMM невалидна.Alexandrhttps://www.blogger.com/profile/01608825627475406437noreply@blogger.comtag:blogger.com,1999:blog-410416665291724878.post-46407161357616708052013-02-15T13:36:50.190+04:002013-02-15T13:36:50.190+04:00Кажется теперь дошло.
12.5. Creation of New Class ...Кажется теперь дошло.<br />12.5. Creation of New Class Instances <br />Just before a reference to the newly created object is returned as the result, the indicated constructor is processed to initialize the new object using the following procedure:<br />...<br />5. Execute the rest of the body of this constructor.<br /><br />Т.е. порядок, вроде как, JLS гарантирует. А про final я, действительно, Anonymoushttps://www.blogger.com/profile/13231616463867351222noreply@blogger.comtag:blogger.com,1999:blog-410416665291724878.post-31719207853513489922013-02-15T13:31:22.065+04:002013-02-15T13:31:22.065+04:00@alexandr
А зависимые по данным инструкции не могу...@alexandr<br />А зависимые по данным инструкции не могут быть переставлены? Почему?Ruslan Chereminhttps://www.blogger.com/profile/01023948540752159657noreply@blogger.comtag:blogger.com,1999:blog-410416665291724878.post-53418455553221676192013-02-15T13:06:09.159+04:002013-02-15T13:06:09.159+04:00Даже так, если говорить о строгой мат модели, наск...Даже так, если говорить о строгой мат модели, насколько корректно аппелировать к байт коду сгенеренным данным конкретным компилятором. Допустимы ли другие варианты компиляции нашей ява программы, при которых публикация не будет отдельным action. Думаю Блох бы ответил просто "не допустимы", но я вот навскидку не готов. Anonymoushttps://www.blogger.com/profile/07493230113211444512noreply@blogger.comtag:blogger.com,1999:blog-410416665291724878.post-22205786455231954242013-02-15T13:02:52.574+04:002013-02-15T13:02:52.574+04:00hb не гарантирует что на практике они будут выполн...hb не гарантирует что на практике они будут выполнены именно в таком порядке. Но гарантируется, что на исполнении програмы эти перестановки не скажутся. Даже из другого потока эта разница не будет видна. А вы сами показываете, что разница видна будет, следовательна такая перестановка недопустима.Anonymoushttps://www.blogger.com/profile/07493230113211444512noreply@blogger.comtag:blogger.com,1999:blog-410416665291724878.post-19805350222275780492013-02-15T12:53:37.858+04:002013-02-15T12:53:37.858+04:002 и 3 не зависит по данным - поэтому теоретически ...2 и 3 не зависит по данным - поэтому теоретически могут быть переставлены.<br />Правильно ли я понимаю, что пользуясь вашим доказательством, в следующем примере будет истина:<br /><br />volatile int i = 0;<br />int j = 0;<br />// thread 1<br />i = 1;<br />j = 1;<br />// thread 2<br />if (j == 1) {<br /> int k = i;<br /> // we know that k = 1<br />}<br />Alexandrhttps://www.blogger.com/profile/01608825627475406437noreply@blogger.comtag:blogger.com,1999:blog-410416665291724878.post-19009917549246999782013-02-15T12:47:26.897+04:002013-02-15T12:47:26.897+04:00Как я понял вопрос Ростислава, тут у нас один пото...Как я понял вопрос Ростислава, тут у нас один поток и вопрос даже не о hb, а о programming order. Это уже конечно занудство, но можно ли воспринимать публикацию ссылки (шаг (3)) как отдельный action не очень понятно из JMM.<br />Например если мы публикуем объект эксепшена инструкцией athrow, является ли это отдельным action? И где это написано в JMM?<br /><br />Если посмотреть во что Anonymoushttps://www.blogger.com/profile/07493230113211444512noreply@blogger.com