Как доказать, что параллельный объект линеаризуем?

Есть ли способ доказать, линеаризуем ли объект? Например, для кода ниже. Как доказать, что счетчик линеаризуем?

вот алгоритм общего счетчика:


CompareAndSet R = new CompareAndSet(0);

increment() {
   Boolean ret; int r;
   repeat r = R.read(); ret = R.cas(r, r+1)
   until(ret = true)
   return
}

read() {
 return R.read();
}

CompareAndSet — это объект, который содержит:

  • целое v
  • метод read(): возвращает значение v
  • метод cas(ожидаемый, обновление): принимает 2 аргумента: значение expected и значение update. Если текущее значение v равно ожидаемому значению, то оно заменяется значением обновления; в противном случае значение остается неизменным. Вызов метода возвращает логическое значение, указывающее, изменилось ли значение v.

concurrency cpu-registers mutual-exclusion
person Sydney.Ka    schedule 03.01.2020    source источник

Ответы (1)


arrow_upward
0
arrow_downward

Вообще говоря, вам нужно показать, что для каждого метода, изменяющего параллельный объект, существует «точка линеаризации», в которой метод вступает в силу.

Для вашего счетчика это тривиально. Если мы предположим, что R.cas() выполняется атомарно, то ваша точка линеаризации в increment() наступит, когда R.cas() успешно обновит значение.

person Eric    schedule 03.01.2020
comment
Как доказать, что точка линеаризации является точкой линеаризации? - person OSEMA TOUATI; 04.01.2020