Снова о статической типизации

Может быть там просто оптимизированный код который ты не осилил?

Ты как обычно.

compilation error

С чего бы? И это мы ещё даже не начали углубляться в самое интересное - когда решения брать мьютекс или нет зависят не только от переданных параметров, но и от состояния самого объекта.

Сущность, которая характеризует ограничения набора значений

Ну передают в твою функцию мьютекс, окей. Мы статически знаем, что это будет мьютекс. А в каком он будет состоянии, как ты узнаешь до того, как программа начнёт выполняться?

С того, что std::optional::reset() не принимает аргумента. У тебя там что-то странное написано

И это мы ещё даже не начали углубляться в самое интересное - когда решения брать мьютекс или нет зависят не только от переданных параметров, но и от состояния самого объекта.

Мне это абсолютно не интересно. Задачу я очертил, и она состоит в том, чтобы однозначно отделить код, выполняющийся под блокировкой, от кода, который выполняется не под блокировкой.

А в каком он будет состоянии, как ты узнаешь до того, как программа начнёт выполняться?

Я выше показал пример.

Нужно monk в тему позвать.

Тема хорошо показывает, почему программирование нужно изучать по книгам типа «C++ for real programmers» by Jeff Alger, ане по самоучителю «Питон для чайников».

Так стремление все мютексы сделать статически используемыми это как раз скорее из питонов.

Кто тебе сказал, что они статически используемые, и что вообще означает термин «статически используемые»?

Необходимо гарантировать, что при любом пути исполнения кода захват и освобождение мьютексов выполняется в фиксированной последовательности, что гарантирует отсутствие деадлоков для данного набора мьютексов.

а что тут сложного? любой гарантированно мьютексированный доступ можно оформить через прокси обьект, навроде прокси ссылки, которая создается с локом мьютекса, и деструктруируется с разлоком.

а зависимость мьютексов по локам делается такими же ссылками, где конструктор принимает ссылку на прокси от предыдущего мьютекса по порядку локов. тогда следующий лок нельзя сделать, если нет предыдущего. и разлок идет в верном порядке

а что тут сложного?

Ничего принципиально сложного, но как видишь, из обсуждения, это несложно только в случае, если ты в целом ухватил идею, как и для чего можно использовать типы данных. Если нет – то появляются вопросы.

Я напомню, что исходно в ОП речь шла о более простой задаче – ограничить возможность вызова ряда функций. Такая задача вполне решаема весьма консервативным образом.

и в чём проблема ? сделай чтобы «незахваченный» объект имел другой интерфейс. (тип/вид/класс...), и чтобы время жизни ограничивалось лексик-скоп.

как с файлами: ты не можешь писать в файл не осуществив операцию «открыть». Как только открыл, стали доступны операции чтение/записи. Программно - это два разных объекта, хотя и оба зовутся в просторечии «файл».

еще про цепочечный лок мьютексов.

можно еще похимичить с наследованием в таких вот прокси-ссылках, помня, что сначала исполняется конструктор базового класса, последовательность выполнения конструкторов и будет последовательностью локов мьютексов.

то есть первая прокси будет лочить первый мьютекс, вторая бужет наследовать класс первой и лочить второй мьютекс, третья - класс второй и лочить третий мьютекс..и так далее.

Для такого и статической типизации не надо

(define (foo)
  (bar) ;; compile-time error
  (let ([lck (lock)])
    (lck 'bar)) ;; compilation successful
  (bar) ;; compile-time error
  (lck 'bar))) ;; compile-time error

Наверно этот «термин» несколько размытый, но я ничего другого не придумал. Если ты ткнёшь в некоторую строчку кода, то ты сможешь однозначно сказать какие мютексы в выбранный момент взяты. Альтернатива же: список взятых мютексов в общем случае зависит от состояния. Как, например, в моём примере выше на момент mutex_unlock(&list->mtx); ты не можешь без анализа переменных знать, залочен ли item->mtx или нет. Разумеется, в данном примере это бесполезная инфомрация, но там ведь мог быть и посложнее код, который лезет в item и что-то в нём делает.

А ещё может быть ситуация, что доступ к переменной регулируется парой мютексов (т.е. оба когда пишем в неё и хотя бы один когда читаем, либо наоборот при условии что пишет только один тред).

Страшно, очень страшно. (c)

А что не так-то?

Да это так, шутка.

А если серьёзно, то со стороны без знания языка не очень понятно, что тут происходит. Если по отношению к символу bar проверка выполняется во время компиляции, то обычно про такое мы говорим, что это язык не динамический.

А если серьёзно, то со стороны без знания языка не очень понятно, что тут происходит.

Так то же, что и у тебя. Снаружи от lck никакого bar нету.

Могу на JS переписать.

function foo() {
  bar(); // err
  {
    lck = lock();
    lck.bar(); // ok
  }
  bar(); // err
  lck.bar; // err
}

На JS это не будет ошибкой времени компиляции.

let пропустил…

Гм… А на JS как вообще компиляцию запустить? На лиспах так работает…

Можно сделать так, чтобы m2 нельзя было взять без m1, m3 без m2 и т.п. Это подойдет под условия или нет?

Никак… Для этого придумали typescript

Я полагаю, это, можно сказать, упрощенный вариант. А в реальности нужно что-то типа такого, чтобы соблюдалось:

unlocked -> m(N1) -> m(N2) ...

Где N1 < N2 < ....

Проблема в том, что в наивной реализации всегда можно (случйно или специально) начать от корня и получить конфликтующую последовательность:

unlocked -> m(2) // далее в том же потоке:
unlocked -> m(1) // контракт использования нарушен

Возможно, вопрос можно решить при помощи большого количества магии на шаблонах, но как конкретно – пока не знаю.

М-да… значит придётся остаться с примером на Racket.

Он компилируется и при компиляции проверяет область видимости. Если нет глобальной функции bar или lck, то без определения в текущем блоке будет ругаться.

Проблема в том, что в наивной реализации всегда можно (случйно или специально) начать от корня и получить конфликтующую последовательность:

Передаём в lock предыдущий параметр. После передачи «портим» его, чтобы пока блокировка не снята, повторно от него не сделать последовательность.

unlocked – глобальная константа, соответственно от неё может быть только одна активная последовательность.

А как ее в компайл тайме «испортить», если язык не поддерживает макросы?

Да, я уже понял, что затупил. Тут только Rust в голову приходит.

В голове вертится что-то насчет монад и хаскеля.

Нужно проверку типов на уровне связывания стейтментов в последовательность. После того как выполнен переход по машине состояний, описывающей мьютексы, любой захват с не подходящего уровня ловится при проверке типа стейтмента.

Что-то такое.

А так как средства хаскеля вполне можно отразить на шаблоны крестов, то и на шаблонах реализация возможна.

Но результат будет мало похож на обычный с++.

В Хаскеле нельзя запретить сделать вторую монаду (кроме IO). А в IO просто последовательность операций относительно реального мира, а не некоего unlocked.

Есть вот такая штука: https://www.tweag.io/blog/2023-01-26-linear-constraints-freeze/

Но у меня на ней мозги плавятся.

выше показал пример

То есть ты хочешь этакие type guards, как в тупоскрипте, основанные на анализе путей выполнения и позволяющие вывести тип, который должно иметь значение, прошедшее или не прошедшее ту или иную проверку (например, сравнение с другим значением). Скажем, сравнили x с null — в одной ветке ифа его тип гарантированно будет null (будет включать одно возможное значение), в другой ветке — тип, из которого удалён null как возможное значение.

И ты думаешь, что у тебя получится таким образом выводить состояние мьютекса. Ну-ну. Что за недоязычок-то хоть?

я давным давно написал такую штуку https://github.com/mdraven/mutex_order/blob/master/main.cpp

Там порядок мьютексов задаётся с помощью MutexOrder, и можно двигаться по порядку с помощью метода lock(…). Например тут:

    template<class Handler>
    int get_then(int key, mutex_order_slice<MutexOrder, MapMutex> mo_slice, Handler &&handler) {
        return mo_slice.lock(_mut, [&](mutex_order_slice<MutexOrder, BMutex> mo_slice) {
            int value = get_from_map(key, mo_slice);
            value += handler(mo_slice);
            return value;
        });
    }

у нас был мьютекс в позиции MapMutex, а мы его подвинули в BMutex. Но с таким подходам есть проблема с контейнерами у которых внутри каждого элемента мьютекс – непонятно как это отразить в типах. Такие дела.

Для подобных вещей можно попробовать использовать примитив синхронизации под названием «Монитор Хоара», но я не помню точно, расставляет ли он что-то на этапе компиляции или нет.

Гм, интерес теоретический или практический?

Я думаю совершенно точно можно описать на Idris, Coq, Agda и т.п. (гм.. а что тут в т.п. положить я даже не в курсе, ребят..) Вполне вероятно получится на Хаскеле и/или Окэмле как уже тут упоминалось.

Может даже на с++ можно описать, но лично я вряд ли смогу навскидку.. я правда задачу не понял.. но это честно говоря уже детали реализации :)

что тут в т.п. положить

кстати, в т.п. как минимум scala.

а потом мутексов станет ДВА..что вполне реальная ситуация

это каким забором придётся городить чтобы «если незалочены оба, то операция даст ошибку в компайл-тайме» ? :-)

Что за недоязычок-то хоть?

Ты C++ не узнал или что? Харош тупить.

Если все возможные операции представить исключительно как типы данных, то тогда возможно описать задачу для N мьютексов как набор допустимых конверсий типов данных.

Как-то так я это вижу.

Гм, интерес теоретический или практический?

По отношению к первой описанной задаче – практический, но её и я так знаю, как решать.

По отношению ко второй – академический.

То есть на шаблонах смысл какой:

Вот так у нас нет контроля над тем, что представляют собой foo и bar:

foo();
bar();

А нам нужно установить связь между операциями в последовательности операций. И эту связь проверять при помощи системы типов.

Вот так связь есть:

foo().bar();

То есть решение должно быть таким, чтобы вся цепочка блокировки-разблокировки была сформулирована как цепочка методов или как цепочка лямбд.

Если не может быть блокировки, которая проживёт дольше, чем такая цепочка, то мы (наверное) сможем описать это как соотношения типов.

https://en.wikipedia.org/wiki/Typestate_analysis

Если прищуриться, эта сова натягивается на

https://en.wikipedia.org/wiki/Substructural_type_system#Affine_type_systems

Что в свою очередь из мейнстримных языков наиболее близко к теории реализовано в… угадай, где?

TL;DR: Молодец, ты изобрёл Rust.

Как же вы, фанатики Раста, задобали своей клонадой.

Ты в принципе умеешь адеватно вести разговор без клоунады, или эта способность пропадает на каком-то этапе?

Я правильно понял, что у тебя последовательность блокировок проверяется в рантайме?

Но с таким подходам есть проблема с контейнерами у которых внутри каждого элемента мьютекс – непонятно как это отразить в типах.

Для однотипных элементов можно использовать захват в порядке их адресов в памяти.

Но со стороны системы типов нужно наложить ограничение, что захват не может выполняется поэтапно на разных уровнях стека. Как это сделать, не очень понятно.

данная задача решаема на статически типизированном языке

Не очень понятно каким образом. Можно пример?

начать с этого

И где тут статическая типизация?

Здесь:

Compile-time error

В Rust это делается паттерном создания структуры состояния на каждое состояние (Typestate Pattern), есть compile time PhantomData для удобства маркировки типа, если я верно задачу понял. Думаю проблемы написать такое же под C++ нет.

Ты про вторую задачу или про первую?