Здравствуйте, vf, Вы писали:

R>>Я достаточно уверен, что это так. И никто пока не оспорил, что это не так.
R>>Грубо говоря, linearizablе — это "ведёт себя как аналогичная структура данных, основанная на мьютексе". Если же для некоторых программ заменить мьютекс очередь на M&S очередь, то они начнут падать.
R>>Эта моя очередь тоже не linearizablе.

vf>Прочитал этот тред, но это более частный случай, аппонент твой не согласился, да и объективно M&S гораздо ближе к linerizable. А где он конкретно спотыкается, что происходит при удалении очереди?

Мой аргумент очень простой — вот пример кода, который прекрасно работает с мьютекс-очередью, заменяем её на M&S очередь — начинает падать. А это есть основное практическое следствие из linearizability — можно спокойно так заменять и не должно быть никаких видимых изменений в поведении. Они доказывали свойство linearizability в неком академическом абстрактном коне в вакууме, в котором объекты не создаются и не удаляются динамически.

struct tcp_connection
{
  queue_t q;
  ...

};

void connection_thread(tcp_connection* c)
{
  for (;;)
  {
    msg_t* m = c->dequeue();
    if (m->type == MSG_DISCONNECT)
    {
      delete c;
      return;
    }
    process(m);
  }

}

void io_dispatch_thread()
{
  for (;;)
  {
    select(...);
    for_each(SOCKET s in read_set)
    {
      recv(s, buf, size);
      tcp_connection* c = find_connection(s);
      c->enqueue(msg_t(MSG_PACKET, data, size));
    }
    for_each(SOCKET s in exception_set)
    {
      tcp_connection* c = find_connection(s);
      c->enqueue(msg_t(MSG_DISCONNECT));
    }
  }
}