LINUX.ORG.RU

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

 ,


1

4

Пример задачи:

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

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

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

Легко сообразить, что данная задача решаема на статически типизированном языке. (С разным уровнем костыльности-некостыльности, в зависимости от того, что это за язык.) И нерешаема на динамически типизированном языке.

Усложненный вариант задачи.

В программе имеются мьютексы m1, m2… mN.

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

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

В таких случаях становится особенно важно переложить на машину настолько много подзадач по формальной верификации алгоритма, насколько вообще возможно.

import multiprocessing as mp

_lock = mp.RLock()

def worker(...):
  ...
  with _lock:
    mp_dict['shit'] = ... 

mp_dict = mp.Manager().dict()

p1 = mp.Process(target=worker, args=(...))
p1.start()

p2 = mp.Process(target=worker, args=(...))
p2.start()

p1.join()
p2.join()
rtxtxtrx ★★
()
Последнее исправление: rtxtxtrx (всего исправлений: 2)

Такая «статическая» проверка называется дебаг :D. Если 100500 if по динамическим условиям влияют на то будет ли сейчас захват или игнор мутекса то хрен чего отловишь. Максимум что можно проверить это проставлены ли вызовы проверки мутекса и его захвата в коде и в том ли порядке, всё. Ну как по мне. А дальше там что угодно может происходить.

Опять же, всё это здорово но установка мутекса ничем не отличается от вызова функции, это не совсем то что вообще относится к типизации как таковой, статическая типизация проверяет конверсию типов из->в и там предупредит про всегла ложный/истинный if, бесконечный цикл или вероятную ошибку вычислений привыполнении, обеспечит упреждающую оптимизацию, а не прочекает всю логику программы.

Это я к тому что типизация тут непричём от слова ваще, тут специализированные тулзы нужны специально проверяющие что некие хни должны быть упорядоченны в вызовах на основе мутексов…

Ой…. Стой, ты имеешь в виду нужно вводить тип? Ну типа

int mutexable foo();
int mutexable bar();

И конпелятор помимо проверок типов должен ещё проверять что мутексаблинутые хехе функции корректно будут захватывать и отпускать блокировки?

LINUX-ORG-RU ★★★★★
()
Ответ на: комментарий от LINUX-ORG-RU

Опять же, всё это здорово но установка мутекса ничем не отличается от вызова функции, это не совсем то что вообще относится к типизации как таковой

Ложки нет, Нео.

wandrien ★★
() автор топика
Ответ на: комментарий от wandrien
with _lock:
  # все что внутри блокируется для модификации другими процессами 

И вот… тупизации нет, а защита есть. К чему тема-то?

rtxtxtrx ★★
()
Последнее исправление: rtxtxtrx (всего исправлений: 1)
Ответ на: комментарий от rtxtxtrx

все что внутри блокируется для модификации другими процессами

Потрясающее открытие. Ты изобрел мьютексы. Поздравляю.

wandrien ★★
() автор топика
Последнее исправление: wandrien (всего исправлений: 1)
Ответ на: комментарий от LINUX-ORG-RU

Ой ладно, я просто почитаю чего тут напишут.

Судя по первым комментариям, тут будут только лулзы и тупак.

Я уже приготовился собирать бинго.

wandrien ★★
() автор топика
Ответ на: комментарий от rtxtxtrx

Молодец. А теперь сделай так, чтобы программа, которая пытается осуществить доступ к mp_dict в обход мьютекса, упала в компайл-тайме.

wandrien ★★
() автор топика
Последнее исправление: wandrien (всего исправлений: 1)

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

alysnix ★★★
()
Ответ на: комментарий от rtxtxtrx

Ну, это можно отнести даже к типу, например что такое проверка на if это когда машина выполняет для значения test инструкцию и в зависимости от этого делается jump или просто продолжает выполнение того что за ним. На уровне абстракций языка можно сказать что это тип, а его крайние значения определяют будет ли выполнена текущая инструкция jmp или нет. Так что в целом можно сказать что блокировка сама по себе это тип и вполне себе проверяемый на этапе разбора языка, но правда я всё равно не вкуриваю в то как оно может гарантированно проверить все случаи with _lock: это равносильно явной установке mutex_lock(m), его можно забыть вписать например, но вот если блок кода пометить выше типа _lock def(...)... тогда уже всё что входит в блок кода должно иметь проверку на блокирвоки внутри и правильную проверку на них или проверятся рантаймом, ты просто вызываешь функцию (кусок кода, байткода, инстуркуий, пофиг чего), а запустится она автоматически тогда когда блокировка будет отпущена и автоматически блокировка будет установлена, то есть в целом ненужно ничего явно указывать, нужно просто сказать что весь этот кусок кода помечен как блокирующий, не явным вызовом блокировки внутри ака семафор, а неявной блокировкой на уровне исполнения котрая гарантирует что хоть ты там навызывайся кого хочшеь в каком угодно порядке выполнено будет всё в порядке очереди захвата блокировки и никак иначе. Но тут типизация уже не на уровне куска памяти в оперативке, а на уровне куска кода.

LINUX-ORG-RU ★★★★★
()
Последнее исправление: LINUX-ORG-RU (всего исправлений: 2)
Ответ на: комментарий от LINUX-ORG-RU

Но тут типизация уже не на уровне куска памяти в оперативке

Да нет никакой типизации: есть лишь байты, которые группируются в какие-то структуры… Все 8-битное число, и даже небо, и даже… Не понимаю всех этих пространных рассуждений ряяя

rtxtxtrx ★★
()
Ответ на: комментарий от LINUX-ORG-RU

Да with - это сахарок над явным вызовАми _lock.acquire и _lock.release, там аналог такого:

_lock.acquire()
try:
  # <код внутри with>
finally:
  _lock.release()
rtxtxtrx ★★
()
Последнее исправление: rtxtxtrx (всего исправлений: 1)
Ответ на: комментарий от rtxtxtrx

Так можно просто сделать любой код через приведение типа сделать блокирующим или наоборот разрешить его произвольное выполнение без учёта блокировок, при этом само тело кода не трогаем от слова вааааще. Ты просто пишешь две функии писать_в_базу() читать_из_базы() просто как есть, но если надо приводишь к блокирующему типу обе функции как через кастование типов и получаешь гарантию последовательной работы обоих функций. Если не нужно кастуешь их/её к обычному состоянию и всё теберь они могут вызываться как попало. В этом чвота есть. Ну, а внизу да, байты,биты как всегда, кто их чтоль отменяет?

Но ты про скриптуху там в рантайме что угодно делать можно, а вот для статических языков это другое, тут тоже самое надо выразить и чтобы работало без рантайма и вирутальной машины, ну или с микрорантайм вставками в исполняемый код который отвечает за всё это вот. Есть же pragma omp parallel OpenMP параллелит код, сама ставит блокировки и гарантирует что всё будет ок. Но это уже другое.

LINUX-ORG-RU ★★★★★
()
Последнее исправление: LINUX-ORG-RU (всего исправлений: 2)
Ответ на: комментарий от cobold

А если статический анализатор не нашел таких путей исполнения кода, то какое из двух утверждений верно?

  • Таких путей нет.
  • Они есть, но анализатор их не нашел.

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

Во втором случае мы получаем гадание на кофейной гуще.

wandrien ★★
() автор топика

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

Не понимаю, как это сделать в языке со статической типизацией без метапрограммирования (макросов). Можно код показать?

Если же используем метапрограммирование, то, теоретически, и в компилируемом языке со строгой динамической типизацией можно получить ошибку на этапе компиляции. Тут важен именно анализ до запуска, а не типизация. Речь, конечно, не о Питоне. Возможно, в каких-то родственниках (реализациях) Лиспа что-то подобное есть.

Kogrom
()
Ответ на: комментарий от wandrien

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

Я не думаю что это возможно в принципе, без ложных срабатываний как ту так и в другую сторону. Runtime sanitizing - всё что остаётся.

bugfixer ★★★★★
()
Ответ на: комментарий от wandrien

В питоне? Да, невозможно.

Да нигде невозможно. Точнее - я с ходу не могу придумать насколько кастрированным должен быть язык чтобы все relevant runtime branches были (а) вИдимы в точках доступа к разделяемому ресурсу, (б) поддающимися статическому анализу.

bugfixer ★★★★★
()
Последнее исправление: bugfixer (всего исправлений: 2)

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

правильно: имеется сущность обладающая интерфейсом. В интерфейсе есть атомарные операции и транзакционные. Мьютекс, это всё-таки уровнем ниже чем то что ТС пытается обсудить.

ТС хочет гарантировать что транзакция обязательно завершится и чтобы обязательно имела метку «начало». И чтобы это гарантировалось языком, чтобы сделать иначе было невозможно не выходя за синтаксис и семантику, не породив ошибку уровня компиляции/трансляции

PS/ ну и типизация тут конечно-же непричём

MKuznetsov ★★★★★
()
Ответ на: комментарий от MKuznetsov

Мьютекс, это всё-таки уровнем ниже чем то что ТС пытается обсудить.

В жизни нередко так и идёт – мы знаем детали реализации, а теперь нужно придумать для неё надежный интерфейс.

wandrien ★★
() автор топика
Ответ на: комментарий от wandrien

Попробуй думать в терминах областей видимости … и задача становится решаемой.

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

bugfixer ★★★★★
()
Ответ на: комментарий от wandrien

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

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

В рантайме и кидай исключения, если мьютекс не захвачен, или типа того.

Nervous ★★★★★
()
Последнее исправление: Nervous (всего исправлений: 1)
Ответ на: комментарий от bugfixer

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

не забываем про указатели и ссылки

Для этого сырые указатели сначала нужно как-то получить.

wandrien ★★
() автор топика
Ответ на: комментарий от Nervous

Откуда иначе компилятору знать, какие значения ты передашь в свою функцию в рантайме?

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

wandrien ★★
() автор топика
Ответ на: комментарий от wandrien

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

Я думаю что мне хватит одного boolean’а переданного извне чтобы развалить любой статический анализатор который Вы можете придумать, максимум - двух.

bugfixer ★★★★★
()
Ответ на: комментарий от bugfixer

Можно начать с этого:

void Foo::foo()
{
    bar(); /* compile-time error */
    {
        LockedContext lck = lock();
        lck.bar(); /* compilation successful */
    }
    bar(); /* compile-time error */
    lck->bar(); /* compile-time error */
}

Разваливайте.

wandrien ★★
() автор топика
Последнее исправление: wandrien (всего исправлений: 1)

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

В программе имеются мьютексы m1, m2… mN.

Если у тебя все мютексы статические то там скорее всего и так всё тривиально. А вот более реальная ситуация: есть экземпляр структуры A, в ней есть мютекс, и есть экземпляр структуры B, на которую есть ссылка из структуры A, и в нём тоже есть мютекс. Надо, чтобы мютекс структуры A не пытался блокированно лочиться во время того как залочен мютекс хотя бы одной из структур B, на которые есть ссылки из A. Как ты это формализуешь в коде? Ну, может быть и сможешь, но там будет write-only ужас.

firkax ★★★★★
()
Ответ на: комментарий от firkax

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

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

wandrien ★★
() автор топика
Последнее исправление: wandrien (всего исправлений: 1)
Ответ на: комментарий от wandrien

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

Вот смотри например:

t_item * _find_item(t_list *list, char const *name, int lock) {
  t_item *item;
  mutex_lock(&list->mtx);
  item = find_item_locked(list, name);
  if(lock) mutex_lock(&item->mtx);
  mutex_unlock(&list->mtx);
  return item;
}

#define get_item(list,name) _find_item(list,name,1)
#define item_exists(list,name) (!!_find_item(list,name,0))
Как ты формально оформишь что в одном случае функция возвращает залоченный item, а в другом - только флаг его существования? Делать две отдельные функции для этого нехорошо т.к. у них одинаковый код и можно в итоге случайно его рассинхронизировать.

firkax ★★★★★
()