История изменений
Исправление wandrien, (текущая версия) :
Про мьютексы.
У нас есть мьютексы с M<1> по M<n>.
Для простоты будем считать, что также есть корневой мьютекс M<0>, который всегда залочен.
Тип, который отражает состояние «мьютекс залочен» – Locked<M<k>>.
Для мьютекса M<0> при запуске программы мы имеем объект mRoot: Locked<M<0>>.
Если у нас имеется залоченный мьютекс k, и мы хотим залочить мьютекст i, где i > k, для этого имеется функция:
lock<M<i>>(mK: Locked<M<k>>) -> (Locked<M<i>>, LockLink<M<k>, M<i>>), where i > k && i <= n
которая поглощает объект типа Locked<M<k>> и возвращает два объекта типов Locked<M<i>> и LockLink<M<k>, M<i>>.
Если мы хотим освободить мьютекст i, для этого имеется функция:
unlock(mI: Locked<M<i>>, link: LockLink<M<k>, M<i>>) -> Locked<M<k>>
которая поглощает объекты типов Locked<M<i>> и LockLink<M<k>, M<i>> и возвращает объект типа Locked<M<k>>.
Типы Locked<M<i>> и LockLink<M<k>, M<i>> являются линейными.
В данном случае достаточно того, чтобы система типов поддерживала линейные типы.
Это что касается порядка захвата и освобождения мьютексов. Если же необходимо одновременно с этим обеспечить решение и первой задачи из ОП (необходимо гарантировать, что заданные функции могут быть вызываны только при заданном захваченном мьютексе), то я вижу несколько вариантов решения в зависимости от того, какие фичи имеет система типов.
P.S.
Также нужна функция, которая в конце алгоритма поглотит корневой mRoot, иначе программа тайпчек не пройдет:
dropRoot(mRoot: Locked<M<0>>) -> void
Исправление wandrien, :
Про мьютексы.
У нас есть мьютексы с M<1> по M<n>.
Для простоты будем считать, что также есть корневой мьютекс M<0>, который всегда залочен.
Тип, который отражает состояние «мьютекс залочен» – Locked<M<k>>.
Для мьютекса M<0> при запуске программы мы имеем объект mRoot: Locked<M<0>>.
Если у нас имеется залоченный мьютекс k, и мы хотим залочить мьютекст i, где i > k, для этого имеется функция:
lock<M<i>>(mK: Locked<M<k>>) -> (Locked<M<i>>, LockLink<M<k>, M<i>>), where i > k && i <= n
которая поглощает объект типа Locked<M<k>> и возвращает два объекта типов Locked<M<i>> и LockLink<M<k>, M<i>>.
Если мы хотим освободить мьютекст i, для этого имеется функция:
unlock(mI: Locked<M<i>>, link: LockLink<M<k>, M<i>>) -> Locked<M<k>>
которая поглощает объекты типов Locked<M<i>> и LockLink<M<k>, M<i>> и возвращает объект типа Locked<M<k>>.
Типы Locked<> и LockLink<> являются линейными.
В данном случае достаточно того, чтобы система типов поддерживала линейные типы.
Это что касается порядка захвата и освобождения мьютексов. Если же необходимо одновременно с этим обеспечить решение и первой задачи из ОП (необходимо гарантировать, что заданные функции могут быть вызываны только при заданном захваченном мьютексе), то я вижу несколько вариантов решения в зависимости от того, какие фичи имеет система типов.
P.S.
Также нужна функция, которая в конце алгоритма поглотит корневой mRoot, иначе программа тайпчек не пройдет:
dropRoot(mRoot: Locked<M<0>>) -> void
Исправление wandrien, :
Про мьютексы.
У нас есть мьютексы с M<1> по M<n>.
Для простоты будем считать, что также есть корневой мьютекс M<0>, который всегда залочен.
Тип, который отражает состояние «мьютекс залочен» – Locked<M<k>>.
Для мьютекса M<0> при запуске программы мы имеем объект mRoot: Locked<M<0>>.
Если у нас имеется залоченный мьютекс k, и мы хотим залочить мьютекст i, где i > k, для этого имеется функция:
lock<M<i>>(mK: Locked<M<k>>) -> (Locked<M<i>>, LockLink<M<k>, M<i>>), where i > k && i <= n
которая поглощает объект типа Locked<M<k>> и возвращает два объекта типов Locked<M<i>> и LockLink<M<k>, M<i>>.
Если мы хотим освободить мьютекст i, для этого имеется функция:
unlock(mI: Locked<M<i>>, link: LockLink<M<k>, M<i>>) -> Locked<M<k>>
которая поглощает объекты типов Locked<M<i>> и LockLink<M<k>, M<i>> и возвращает объект типа Locked<M<k>>.
В данном случае достаточно того, чтобы система типов поддерживала линейные типы.
Это что касается порядка захвата и освобождения мьютексов. Если же необходимо одновременно с этим обеспечить решение и первой задачи из ОП (необходимо гарантировать, что заданные функции могут быть вызываны только при заданном захваченном мьютексе), то я вижу несколько вариантов решения в зависимости от того, какие фичи имеет система типов.
P.S.
Также нужна функция, которая в конце алгоритма поглотит корневой mRoot, иначе программа тайпчек не пройдет:
dropRoot(mRoot: Locked<M<0>>) -> void
Исправление wandrien, :
Про мьютексы.
У нас есть мьютексы с M<1> по M<n>.
Для простоты будем считать, что также есть корневой мьютекс M<0>, который всегда залочен.
Тип, который отражает состояние «мьютекс залочен» – Locked<M<k>>.
Для мьютекса M<0> при запуске программы мы имеем объект mRoot: Locked<M<0>>.
Если у нас имеется залоченный мьютекс k, и мы хотим залочить мьютекст i, где i > k, для этого имеется функция:
lock<M<i>>(mK: Locked<M<k>>) -> (Locked<M<i>>, LockLink<M<k>, M<i>>), where i > k && i <= n
которая поглощает объект типа Locked<M<k>> и возвращает два объекта типов Locked<M<i>> и LockLink<M<k>, M<i>>.
Если мы хотим освободить мьютекст i, для этого имеется функция:
unlock(mI: Locked<M<i>>, link: LockLink<M<k>, M<i>>) -> Locked<M<k>>
которая поглощает объекты типов Locked<M<i>> и LockLink<M<k>, M<i>> и возвращает объект типа Locked<M<k>>.
В данном случае достаточно того, чтобы система типов поддерживала линейные типы.
Это что касается порядка захвата и освобождения мьютексов. Если же необходимо одновременно с этим обеспечить решение и первой задачи из ОП (необходимо гарантировать, что заданные функции могут быть вызываны только при заданном захваченном мьютексе), то я вижу несколько вариантов решения в зависимости от того, какие фичи имеет система типов.
Исправление wandrien, :
Про мьютексы.
У нас есть мьютексы с M<1> по M<n>.
Для простоты будем считать, что также есть корневой мьютекс M<0>, который всегда залочен.
Тип, который отражает состояние «мьютекс залочен» – Locked<M<k>>.
Для мьютекса M<0> при запуске программы мы имеем объект mRoot: Locked<M<0>>.
Если у нас имеется залоченный мьютекс k, и мы хотим залочить мьютекст i, где i > k, для этого имеется функция:
lock<M<i>>(mK: Locked<M<k>) -> (Locked<M<i>>, LockLink<M<k>, M<i>>), where i > k && i <= n
которая поглощает объект типа Locked<M<k>> и возвращает два объекта типов Locked<M<i>> и LockLink<M<k>, M<i>>.
Если мы хотим освободить мьютекст i, для этого имеется функция:
unlock(mI: Locked<M<i>>, link: LockLink<M<k>, M<i>>) -> Locked<M<k>>
которая поглощает объекты типов Locked<M<i>> и LockLink<M<k>, M<i>> и возвращает объект типа Locked<M<k>>.
В данном случае достаточно того, чтобы система типов поддерживала линейные типы.
Это что касается порядка захвата и освобождения мьютексов. Если же необходимо одновременно с этим обеспечить решение и первой задачи из ОП (необходимо гарантировать, что заданные функции могут быть вызываны только при заданном захваченном мьютексе), то я вижу несколько вариантов решения в зависимости от того, какие фичи имеет система типов.
Исправление wandrien, :
Про мьютексы.
У нас есть мьютексы с M<1> по M<n>.
Для простоты будем считать, что также есть корневой мьютекс M<0>, который всегда залочен.
Тип, который отражает состояние «мьютекс залочен» – Locked<M<k>>.
Для мьютекса M<0> при запуске программы мы имеем объект root: Locked<M<0>>.
Если у нас имеется залоченный мьютекс k, и мы хотим залочить мьютекст i, где i > k, для этого имеется функция:
lock<M<i>>(mK: Locked<M<k>) -> (Locked<M<i>>, LockLink<M<k>, M<i>>), where i > k && i <= n
которая поглощает объект типа Locked<M<k>> и возвращает два объекта типов Locked<M<i>> и LockLink<M<k>, M<i>>.
Если мы хотим освободить мьютекст i, для этого имеется функция:
unlock(mI: Locked<M<i>>, link: LockLink<M<k>, M<i>>) -> Locked<M<k>>
которая поглощает объекты типов Locked<M<i>> и LockLink<M<k>, M<i>> и возвращает объект типа Locked<M<k>>.
В данном случае достаточно того, чтобы система типов поддерживала линейные типы.
Это что касается порядка захвата и освобождения мьютексов. Если же необходимо одновременно с этим обеспечить решение и первой задачи из ОП (необходимо гарантировать, что заданные функции могут быть вызываны только при заданном захваченном мьютексе), то я вижу несколько вариантов решения в зависимости от того, какие фичи имеет система типов.
Исправление wandrien, :
Про мьютексы.
У нас есть мьютексы с M<1> по M.
Для простоты будем считать, что также есть корневой мьютекс M<0>, который всегда залочен.
Тип, который отражает состояние «мьютекс залочен» – Locked<M<k>>.
Для мьютекса M<0> при запуске программы мы имеем объект root: Locked<M<0>>.
Если у нас имеется залоченный мьютекс k, и мы хотим залочить мьютекст i, где i > k, для этого имеется функция:
lock<M<i>>(mK: Locked<M<k>) -> (Locked<M<i>>, LockLink<M<k>, M<i>>), where i > k && i <= n
которая поглощает объект типа Locked<M<k>> и возвращает два объекта типов Locked<M<i>> и LockLink<M<k>, M<i>>.
Если мы хотим освободить мьютекст i, для этого имеется функция:
unlock(mI: Locked<M<i>>, link: LockLink<M<k>, M<i>>) -> Locked<M<k>>
которая поглощает объекты типов Locked<M<i>> и LockLink<M<k>, M<i>> и возвращает объект типа Locked<M>.
В данном случае достаточно того, чтобы система типов поддерживала линейные типы.
Это что касается порядка захвата и освобождения мьютексов. Если же необходимо одновременно с этим обеспечить решение и первой задачи из ОП (необходимо гарантировать, что заданные функции могут быть вызываны только при заданном захваченном мьютексе), то я вижу несколько вариантов решения в зависимости от того, какие фичи имеет система типов.
Исходная версия wandrien, :
Про мьютексы.
У нас есть мьютексы с M<1> по M.
Для простоты будем считать, что также есть корневой мьютекс M<0>, который всегда залочен.
Тип, который отражает состояние «мьютекс залочен» – Locked<M<k>>.
Для мьютекса M<0> при запуске программы мы имеем объект root: Locked<M<0>>.
Если у нас имеется залоченный мьютекс k, и мы хотим залочить мьютекст i, где i > k, для этого имеется функция:
lock<Locked<M<k>>, M<i>> -> (Locked<M<i>>, LockLink<M<k>, M<i>>), where i > k && i <= n
которая поглощает объект типа Locked<M<k>> и возвращает два объекта типов Locked<M<i>> и LockLink<M<k>, M<i>>.
Если мы хотим освободить мьютекст i, для этого имеется функция:
unlock<Locked<M<i>>, LockLink<M<k>, M<i>>> -> Locked<M<k>>
которая поглощает объекты типов Locked<M<i>> и LockLink<M<k>, M<i>> и возвращает объект типа Locked<M>.
В данном случае достаточно того, чтобы система типов поддерживала линейные типы.
Это что касается порядка захвата и освобождения мьютексов. Если же необходимо одновременно с этим обеспечить решение и первой задачи из ОП (необходимо гарантировать, что заданные функции могут быть вызываны только при заданном захваченном мьютексе), то я вижу несколько вариантов решения в зависимости от того, какие фичи имеет система типов.