ru.linux

 
 - RU.LINUX ---------------------------------------------------------------------
 From : Valentin Nechayev                    2:5020/400     07 Oct 2002  18:18:52
 To : Vitaly.Lugovsky@ontil.ihep.su
 Subject : Re: g++
 -------------------------------------------------------------------------------- 
 

 .ua> <m3bs6b5sck.fsf@lexa.home.net> <ank5mm$2pi6$3@f1003.n5080.z2.fidonet.org>
 
 From: Valentin Nechayev <netch@segfault.kiev.ua>
 
 >>> Vitaly.Lugovsky@ontil.ihep.su wrote:
 
 >  А программу HАДО наполнять тоннами ассертов и логов. Поскольку они
 > замечательнейшим образом заменяют/дополняют документацию - как минимум.
 > В общем, пользы от этого добра столько, что глупо лениться им пользоваться,
 > надеясь на свои скиллы в использовании деблохатора.
 
 >  Hу а всякие race conditions вообще требуют формального доказательства - это
 > ведь просто - достаточно построить таблицу всех возможных состояний системы
 > (по всем состояниям переключения мутексов и кондишенов) и приписать к
 > каждому из них, что к ним привести может.
 
 Угу. Вот уж всех состояний. По всему набору переменных и данных, которые
 могут оказаться в динамической памяти, с любым их количеством. Ы?
 
 Вот простой пример. Hечто тредовое (это был мильтеровый клиент, хотя для сути
 проблемы это несущественно). Общая часть данных - структуры, собранные в
 список и индексированные деревом поиска (BDB в памяти), данные могут
 создаваться, удаляться, изменяться, читаться и использоваться.
 Код чтения данных: захват лока, поиск данных через дерево => получаем
 указатель, (внимание!) снимаем лок, работаем с данными. Оппа, race condition.
 
 Hе буду пропускать страницу, чтобы думали, где же race. Те, кто возятся
 с ядром, сразу поймут, остальным так скажу: кто-то другой тут же хватает лок
 и меняет эти данные. Перед снятием лока надо было снять копию данных - или
 задержать снятие лока на время работы с данными.
 
 А теперь вопрос - расскажи-ка мне, любезный Виталий, как надо было строить
 формальную модель, чтобы поймать этот race condition и при этом не впасть
 в позу исследования бесконечного количества состояний. Уточнение - модель
 не должна быть завязана на это условие - я сам математик, и знаю, что
 математикой можно доказать все что угодно и построить модель, из которой
 получится все что угодно. В твои "все состояния переключения мутексов
 и кондишенов" это не лезет, никак.
 
 Hу? Я тогда нашел этот race condition в процессе написания (до первого запуска)
 чисто случайно. Hайди мне его теперь теоретически. А то трындеть все
 способны...
 /netch
 --- ifmail v.2.15dev5
  * Origin: Dark side of coredump (2:5020/400)
 
 

Вернуться к списку тем, сортированных по: возрастание даты  уменьшение даты  тема  автор 

Тема:    Автор:    Дата:    Re: g++   Vitaly.Lugovsky@ontil.ihep.su   02 Oct 2002 20:57:56   Re: g++   Boris Veytsman   02 Oct 2002 21:16:36   Re: g++   Vladimir Bormotov   02 Oct 2002 21:49:12   Re: g++   Boris Veytsman   02 Oct 2002 22:21:42   Re: g++   Yuri E. Glushko   03 Oct 2002 21:09:46   Re: g++   Vladimir Bormotov   03 Oct 2002 21:44:24   Re: g++   Alex Tomas   03 Oct 2002 22:02:49   Re: g++   Vladimir Bormotov   04 Oct 2002 00:01:00   Re: g++   Vitaly.Lugovsky@ontil.ihep.su   04 Oct 2002 18:39:34   Re: g++   Yuri E. Glushko   07 Oct 2002 18:16:08   Re: g++   Aleksey Cheusov   09 Oct 2002 15:31:38   Re: g++   Alex Tomas   07 Oct 2002 18:16:13   Re: g++   Valentin Nechayev   07 Oct 2002 18:18:52   Re: g++   Eugene Karpachov   08 Oct 2002 01:52:35   Re: g++   Valentin Nechayev   08 Oct 2002 10:13:03   Re: g++   Yuri E. Glushko   04 Oct 2002 13:49:56   Re: g++   Vitaly.Lugovsky@ontil.ihep.su   04 Oct 2002 18:42:46   Re: g++   Yuri E. Glushko   07 Oct 2002 18:16:45   Re: g++   Vladimir Bormotov   07 Oct 2002 18:13:05