SP
ну и да, если система внутри себя много данных из IO генерирует (часы, uuid, random numbers) то тут модель сложно будет построить пожалуй
Size: a a a
2020 September 25
AK
держать все в одном генсервере и делать все операции строго по очереди
AK
они из коробки будут все по очереди
AK
каждую операцию снабдить ключем идемпотентности и синкать на диск после каждой транзакции
P
держать все в одном генсервере и делать все операции строго по очереди
Горлышко
AK
причем ответ выдавать только после успешного синка
SP
с транзакциями у нас лично проблем нет. БД транзакционная, операции строго по порядку. Баги были именно в бизнес-логике
AK
Горлышко
для финансовой транзакции не горлышко
AK
это то как я вижу это делать
AK
и безнес логику в виде дерева, а не графа. Тогда не будет странностей
SP
для финансовой транзакции не горлышко
у нас в системке есть такой ген-сервер. Называется mnesia locker - рулит локами БД, он один единственный на весь кластер из 6 машин по 64 ядра, 512ГБ памяти каждая...
из за него новые страны раскатывают на Java системе с Oracle, а на нашей уже только то что исторически… (Ну, не совсем так, но упрощённо...)
из за него новые страны раскатывают на Java системе с Oracle, а на нашей уже только то что исторически… (Ну, не совсем так, но упрощённо...)
AK
Дерево просто тестится.. как тестить граф вообще фиг знает
ML
т.е. да, состояние зависит только от того, какие мы дёргаем операции
детерминированный конечный автомат — это очень простая математическая конструкция, которая устроена так: ты подаешь ей слово из входного словаря на вход, дальше в нём есть карта сопоставления
Список состояний конечен, словари входные и выходные конечны.
Для такой конструкции есть теорема, которая гласит о том, что за конечное число входных слов можно восстановить карту переходов, т.е. по сути провести полное тестирование.
К реальным компьютерам это малоприменимо, потому что состояний слишком много: 2^количество бит памяти
(Состояние,ВходноеСлово) -> (НовоеСостояние,ВыходноеСлово)Список состояний конечен, словари входные и выходные конечны.
Для такой конструкции есть теорема, которая гласит о том, что за конечное число входных слов можно восстановить карту переходов, т.е. по сути провести полное тестирование.
К реальным компьютерам это малоприменимо, потому что состояний слишком много: 2^количество бит памяти
AK
у нас в системке есть такой ген-сервер. Называется mnesia locker - рулит локами БД, он один единственный на весь кластер из 6 машин по 64 ядра, 512ГБ памяти каждая...
из за него новые страны раскатывают на Java системе с Oracle, а на нашей уже только то что исторически… (Ну, не совсем так, но упрощённо...)
из за него новые страны раскатывают на Java системе с Oracle, а на нашей уже только то что исторически… (Ну, не совсем так, но упрощённо...)
я имел в виду один процес одна транзакция, а не один процесс на все транзакции
SP
детерминированный конечный автомат — это очень простая математическая конструкция, которая устроена так: ты подаешь ей слово из входного словаря на вход, дальше в нём есть карта сопоставления
Список состояний конечен, словари входные и выходные конечны.
Для такой конструкции есть теорема, которая гласит о том, что за конечное число входных слов можно восстановить карту переходов, т.е. по сути провести полное тестирование.
К реальным компьютерам это малоприменимо, потому что состояний слишком много: 2^количество бит памяти
(Состояние,ВходноеСлово) -> (НовоеСостояние,ВыходноеСлово)Список состояний конечен, словари входные и выходные конечны.
Для такой конструкции есть теорема, которая гласит о том, что за конечное число входных слов можно восстановить карту переходов, т.е. по сути провести полное тестирование.
К реальным компьютерам это малоприменимо, потому что состояний слишком много: 2^количество бит памяти
ну да, в этом смысле конечный автомат. И если на вход подать одну и ту же последовательность операций с теми же аргументами 10 раз, результат каждый раз будет одинаковый (ну, может какие-то минорные детали отличаются)
LW
Мы делали модел-чекинг на SPIN/Promela. Пишешь модель на подмножестве Си (Promela), затем спинчекер елозит по state space и проверяет все углы. Выявило как минимум одну проблему.
LW
Чуть поэргономичнее, чем TLA+, кмк.
ИИ
детерминированный конечный автомат — это очень простая математическая конструкция, которая устроена так: ты подаешь ей слово из входного словаря на вход, дальше в нём есть карта сопоставления
Список состояний конечен, словари входные и выходные конечны.
Для такой конструкции есть теорема, которая гласит о том, что за конечное число входных слов можно восстановить карту переходов, т.е. по сути провести полное тестирование.
К реальным компьютерам это малоприменимо, потому что состояний слишком много: 2^количество бит памяти
(Состояние,ВходноеСлово) -> (НовоеСостояние,ВыходноеСлово)Список состояний конечен, словари входные и выходные конечны.
Для такой конструкции есть теорема, которая гласит о том, что за конечное число входных слов можно восстановить карту переходов, т.е. по сути провести полное тестирование.
К реальным компьютерам это малоприменимо, потому что состояний слишком много: 2^количество бит памяти
еще в фунциональной теории чистая функция есть
P
еще в фунциональной теории чистая функция есть
Для неё есть ещё условия помимо детерменированности
AB
код системы никак не переделывали, но пришлось добавить моки в тех местах где оно генерировало уникальные id объектов, чтоб id были предсказуемыми (но вроде есть способы как этого избежать, какие-то shim, но мы по старой привычке сделали).
Насчёт конечного автомата не сильно понял. Стейт это, упрощённо, 3 типа объектов: Debt, Fee, Account. Debt ожет быть отдельностоящий, может быть перемещён на Account. Fee может быть только частью Account. И операции типа "перемести Debt с/на/между Account", "добавь/удали Fee", "пришел платежь, распредели его по Debt" "пользователь решил вернуть часть товаров из debt, а оно уже частично оплачено - перераспредели деньги на другие Debt/Fee" "пользователь не платит, давайте спишем всё" "пользователь заявляет что не получил товар, поставим debt на паузу" и т.п.
Основное что проверяем это конечно цифры долга. Но и есть всякие другие поля на объектах. Ещё каждая операция создаёт какое-то количество эвентов в Kafka, их тоже валидируем (но это скорее как бонус сбоку).
Само оно никуда не ходит, это правда
Насчёт конечного автомата не сильно понял. Стейт это, упрощённо, 3 типа объектов: Debt, Fee, Account. Debt ожет быть отдельностоящий, может быть перемещён на Account. Fee может быть только частью Account. И операции типа "перемести Debt с/на/между Account", "добавь/удали Fee", "пришел платежь, распредели его по Debt" "пользователь решил вернуть часть товаров из debt, а оно уже частично оплачено - перераспредели деньги на другие Debt/Fee" "пользователь не платит, давайте спишем всё" "пользователь заявляет что не получил товар, поставим debt на паузу" и т.п.
Основное что проверяем это конечно цифры долга. Но и есть всякие другие поля на объектах. Ещё каждая операция создаёт какое-то количество эвентов в Kafka, их тоже валидируем (но это скорее как бонус сбоку).
Само оно никуда не ходит, это правда
я правильно улавливаю, что в тестах описывается референсная модель, потом в нее и в реальный инстанс идет флуд командами с сравнением итогового стейта, а потом это всё как-то сводится к минимальной последовательности команд для воспроизведения?