Если осилите HoL, то скорее всего вам не потребуются объяснения. Эти "сектанты" называются прикладными математиками.

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

А реальному программису надо хотя бы узнать как в действительности работает API.
Само изучение API превращается в исследование. Так же с аппаратными ресурсами.
"Прикладные математики" здесь отдыхают.

Я даже готов с вами отчасти согласится о ненужности этого для простого кодера и/или для изделий без ответственности. Ну а кто-то другой возможно возьмет из этой дискуссии больше.

Даже в этом случае такой гарантии не дадите, если только не мигание светодиодом через программную задержку.

Люди даже в "hellо world" умудряются ошибки вывода в терминал делать...

Потому что "Задача покрытия" относится к задачам NP-класса. Поэтому в общем виде не решается за обозримое время

Не, не то.
Они тестировали спецификацию, а не программу.
Представляете!? Есть чудаки которые сначала пишут спецификацию, тестируют ее каким-то образом с хаскелем, и только потом делают из нее программу.
Но ту программу уже не тестируют.
Эт все равно как если б вы для ваших соленоидов сначала придумали диаграммы состояний и переходов между ними с кучей всяких условий и таймингов, а потом решили проверить нет ли там дидлоков в этой диаграмме.
До реальной программы еще как до луны, но куча работы уже проделана, можете идти требовать надбавку.

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

Ну и вы я так понимаю статьи не читали, но мнение имеете?

Вы сами-то докажите что что-то поняли?
От вас только ссылки. Такие мы и сами вам можем тонну отгрузить.

Если бы вы прочитали первую ссылку, вас бы не пришлось отправлять в раздел 4.3. Но с учетом того что вы не осилил даже это, я в обсуждении с вами в серьезном ключе смысла не вижу. Вы ведь всё равно будете фантазировать любую фигню лишь бы сделать вид что это не вы "не ослили", а "авторы дураки".

Не то чтобы авторы дураки, но скорее не ориентируются в теме те кто дает ссылки на такие работы.
Скажем можете ли вы объяснить зачем нам вот такое доказательство - confidentiality and intransitive non-interference proofs?
Т.е. как его применить программисту embedded шлюза между Ethernet и SPI ?

Так насчет вашего первого контраргумента что C код не совпадает с верифицируемым, вы признаете что его придумали?

Нет, конечно.
Если бы действительно читали документ на который ссылаетесь, то знали бы что они сделали код для x86 и его даже не думали проверять.
Да и для ARM они не указали платформу на которой прогоняли код. Это все симуляция.
По ходу это кажется я вам объясняю, как там все устроено.

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

Народ все это интересно, но может стоит обсуждать в отдельной теме? Так как к моей теме я не вижу отношения.

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


Ага, теперь сами признайтесь, я прав?

А какие проблемы-то? (я к вопросу темы)
Фоновый поток не реалтайм, а приоритетные потоки - реалтайм.
Тут нет никакой проблемы.
А проблема в том, чтобы при наличии вытесняющей многозадачности низкоприоритетным потокам тоже гарантировать пусть и бОльшее, чем высокоприоритетным потокам, но ГАРАНТИРОВАННОЕ время реакции.

Это проблема хоть и сложней, но вполне решаема.
Я в разработанной мной RTOS её решил

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

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

Чем гарантирует время реакции? Своим честным словом?

Да вам везет, у меня винда хоть редко, да зависнет, или ФС слетит при некорректном завершении...

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

Ну хотя бы доступ к ресурсам железа, не?

Для AlexandrY

И каким же образом она гарантирует реальное время? Неужели честным словом Билла Гейтса? - мне правда интересно.
Никогда с реальным временем не работал. А как другие гарантируют?


То что они приходят неизвестно когда и в не своё время. Хотя это можно отрегулировать выше стоящей системой. Как следствие состояние системы неизвестно и окромя как выставить собственный флаг в прерывание вы более ничего не можете. Затем вы должны выйти из прерывания. И если это ОС с вытесняющей многозадачностью, то она должна при первом возможном случае вернуться к обработке прерывания, но уже в определённом состоянии:
а) откладываем текущую и начинаем драйверную задачу.
б) дождаться APC и втиснуть прерывание.
с) синхронизироваться с основным циклом секвенсера.

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

Если поток прерываний слишком большой, он "забьёт" более низкоприоритетные, но все равно реал-таймовые задачи.

Я пошёл по пути гарантированного тайм-слота для задач с приоритетами класса 2


С цитированием по внимательней будьте.
Я так понял, это Вы к вот этому:

А не к тому, что процитировали

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

Ну и что?
Проблему решил просто: взял проц с более высокой (на 500% выше чем нужно для моих задач) тактовой. И что? сейчас процессоры стоят дешевле грязи. А вот софт к ним стоит огого. Поэтому лучше купить проц подороже, но сэкономить на софте

Зато реализация RTOS получилась очень простой, красивой и надёжной. И жесткий реалтайм получился ГАРАНТИРОВАННЫМ при вытесняющей многозадачности

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

Проблема дедлоков тоже была решена за счет выбора архитектуры построения RTOS

Таким образом у моей RTOS был только один "минус": 70% времени процессора занимал микродиспетчер, находившийся в таймерном прерывании. Т.е. на диспетчеризацию уходило 70% процессорного времени, а на выполнение "полезной работы" - всего 30%. Но с этим можно смириться. Выбрав более мощный проц

Это невозможно по логике. Подумайте еще раз над этой формулировкой. Время не резиновое.

Возможно.
Я даже объяснил как.
Прочитайте несколько раз, что я написал.
Не всегда и не всем с первого раза доходит

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

Если говорить о многозадачности, то у меня будет Rate-Monotonic Scheduling, который как раз благодаря отсутствию операционки у меня реализуется на ура. Считаю, что тут изобретать нечего - хотя он, возможно, не самый эффективный по загрузке процессора - до 70%, зато гарантирует все то, что мне нужно.

Поэтому я и пошёл по пути запрета всех прерываний кроме таймерного.
А другие прерывания опрашивал по механизму поллинга.
Я же писал: у меня проц больше 70% времени сидит в обработчике таймерного прерывания, а на "полезную работу" доступно менее 30% процессорного времени.

Кто-то скажет: это же не рационально, глупо, криво и т.п.
А я скажу: процессорное время стоит на ПОРЯДКИ дешевле, чем труд программиста.
И это мизерная цена за простоту и прозрачность кода и обеспечение жесткой реалтаймовости при вытесняющей многозадачности и многопоточности


Да плевать на загрузку процессора. Он же железный, вот и пусть пашет.
Труд программиста стоит на порядки дороже чем процессорные такты.
Я когда-то болел болезнью: экономить каждый такт CPU, старался писать код так, чтобы экономить такты. А потом понял, что моё время бесценно, а процессорное стоит копейки.

Фигасе!. Что за такое таймерное прерывание?
В двух словах как работает preemptive real-time операционная система. Ядро получает возможность переключить задачу при системном вызове и после обработки прерывания.
Прерывания читают из железа (и пишут в железо) и разрешает семафор достаточно высокоприоритетной задаче, которая как бы является продолжением прерывание, поскольку при выходе из прерывания обработка будет переключена на нее если исполнялясь низкоприоритетная задача, но прерывания уже не будет.
Еще раз. Бежала какая-то низкоприоритетная задача, когда возникло условие для прерывания. Скажем приняли пакет данных в регистры приемника. В прерывании эти регистры копируются в буфер, буфер ставится в очередь буферов и отпускается семафор обработчика принятого буфера. Все. Выходим из прерывания. Эта работа достаточно короткая и в прерывании больше продолжать не надо. Отпущеный семафор меняет условия для ядра и из прерывания вы выходите не в ту задачу, что исполнялясь, а в ту, которая ждала семафора, поскольку ей нечего было обрабатывать. Фактически вы продолжаете обрабатывать прием, но уже не в прерывании.
Закон. Прерывания надо предельно минимизировать. Обработчик таймера, который считает время, вообще должен инкрементировать счетчик и выйти. Ну еще пару таких же простых операций если очень нужно. И все.

Поллинг самое нехорошее решение для реал тайма.
Если писать правильно, то все будет эффективно и с маленькими затратами. Я пару лет назад пытался описать принципы написания програм реального времени, но отчего-то публика начала возмущаться моей нескромностью и топик в котором я начал описывать технику написания програм реального времени перенесли в тему общение. Как мне объяснили, что раз меня не спрашивают, то и нефиг соваться. Так что если вам интересно -- создайте тему. Скажем "Как писать программы реального времени?", а люди будут вам отвечать. Вот тогда у вас будет пища для принятия решений.

Так обработчики прерываний надо рассматривать как фрагменты задач если придерживаться концепции Rate-Monotonic Scheduling ?
Я вот это не понял.
Если смотреть на них, как на фрагменты задач, то тогда ваш подход прямо нарушает принцип монолитности.
Если же прерывания не фрагменты задач, а нечто другое, то какой принцип планирования применить к обработчикам прерываний.
И не будет ли он конфликтовать с Rate-Monotonic Scheduling?
Исходим из того что обработчики прерываний в высоконагруженной встраиваемой системе исчисляются десятками и занимают больше половины процессорного времени.

Интересный вопрос. Вот, допустим, у меня есть два CAN интерфейса, по которым в любой момент могут быть приняты данные, которые нужны одной или нескольким задачам, выполняющимся по RMS. То есть есть новые данные или их нету, задача все равно выполнится в нужное время. Таким образом задача обработчика прерывания приемника CAN - это всего лишь вытащить данные из приемного буфера и обновить нужные переменные, которые используются в задачах.
Тут есть несколько подводных камней. Если чтение из буфера и обновление переменных сделать высокоприоритетной задачей или сразу в прерывании от CAN, то может случиться так, что это произойдет во время выполнения задачи, которая использует эти переменные. У меня это решено так, что каждая задача читает свои входные переменные только один раз вначале цикла и дальше работает только с внутренними переменными. Тогда обновление входных переменных во время исполнения этой задачи не приведет к непредсказуемым результатам.
Либо как бы второй вариант - делаем обработчик буфера самым низкоприоритетным процессом, тогда он не сможет прервать выпоняющуюся задачу и испортить ей данные. Но тогда, если оставшегося времени не хватит, чтобы обработать весь входной буфер, получим ой.

В таком режиме о энергосбережении можно забыть навсегда. В АВРках или простеньких АРМ, на частоте до 100МГц - это наверно и нафиг не нужно, но на частотах 500+ это очень заметно получается.
На счет труда программиста - для себя не вижу никакой трудности использовать прерывания, нежели изврат с поллингом, но тут дело вкуса, конечно...

Какие Ваши годы. У Вас ещё всё впереди.
"О сколько нам открытий чудных..."
Трудностей нет пока задачи относительно простенькие и проц мощный. И устройство не "mission critical"
Только потом не говорите, что я Вас не предупреждал

Своя ОС, проц мощный, работа в режиме 24\7, полет нормальный...

Спасибо, предупрежден

Тут вы сделали себе логичекую ловушку.
Если вы утверждаете, что обработчик пакетов CAN работает у вас в реальном времени, то вам не надо ничего читать в прерывании. В прерывании только взводите флаг наличия пакета.
Читаете пакет и выполняет действия связанные с ним в единой задаче активизирующейся по флагу. Нет необходимости в промежуточной буферизации.
Буферизация, а лучше ковееризация - верный признак отсутствия реального времени.
Обработчик CAN следовательно не работает у вас в реальном времени.
Итого имеем ситуацию - есть ISR который не задача, и есть задача которая не realtime.

Moderator: Уважаемые, настоятельно призываю вернуть дискуссию в конструктивное русло. Иначе буду наказывать.

Не очень понял, перефразируйте? Обработчик пакетов CAN читает пакет из приемного буфера(или почтового ящика, если так более понятно) приемника CAN, как только тот оказывается там. Других буферов нет.

Вы допустили возможность прихода нового пакета пока не обработан предыдцщий. А это и есть нарушение реального времени.
Т.е. вы на самом деле не работаете в реальном времени. У вас нет жестко специфицированного дедтайма.

Хоть я и ваш собесденик, но нет. Это не нарушение.
Физический канал связи может быть быстрее, чем возможности по его обработке. Внутри железок, кстати, очень часто так - шина гораздо быстрее, чем подключенные к ней периферийные устройства. Но эти устройства выполняют свою функцию за вполне детерминированное время.

Так и здесь - шина CAN способна передавать данные быстрее, чем устройство успевает их обрабатывать. И это нормально: шина не является бутылочным горлышком. А вот ваша уверенность в том, что нельзя при этом принимать/передавать пакет данных, а необходимо пользоваться исключительно одиночными транзакциями - это очень странное и даже вредное убеждение.

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

Тогда нарушаете принцип RMS. Задача должна быть монолитна. А у вас часть задачи в прерывании, часть в потоке. А между ними может вклиниться другая задача или прерывание.
Да что уж там, признайтесь, никакой вы RMS не используете, правда? Так просто, слышали звон.

Я собираюсь использовать RMS. Если так хочется сделать задачу монолитной, то можно спокойно собирать все CAN-пакеты в буфер, а затем обработать их скопом в самой приоритетной задаче, не нарушая принципов RMS.
Но это все сводится к тому, как привести асинхронные задачи (такие как обработка CAN-пакетов) к синхронным - т.е. задачам в RMS. У вас есть другие решения данной проблемы?

Занимаюсь задачами реального времени не один десяток лет, но никогда не слышал о необходимости делать задачи монолитными. "Откуда мол и что это за географические новости"?

Гугл тоже не в курсе:
https://www.google.ca/search?dcr=0&q=Re...427&bih=836

Ссылка в тему, спасибо.
К вопросу о монолитности задач. Это вытекает из принципа анализа RMS.
А главная вещь в том анализе - дидлайн.
Значит нет никакого смысла разбивать задачу на два этапа - сначала взять быстро ее данные, потом медленно данные обрабатывать.
Это все равно что поставить себе целью фальшивый дидлайн, а на самом деле иметь гораздо более отдаленный дидлайн. Обман самого себя.
Такие финты в анализе RMS учтены быть не могут.

По вашей ссылке я вышел на более интересную статью - Rate Monotonic vs. EDF: Judgment Day
Она немного открывает глаза и кстати упоминает подход от "Студент заборстр..."

Подход очень зависит от того, ГДЕ будет использоваться RTOS.
Одно дело в управлении кофемолкой, то там можно гнаться за красотой реализации, использовать какие-то новомодные концепции тащась от собственной крутости.
Вообще по разному можно выпендриваться.

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

Я тоже в своё время игрался с разными концепциями, соблазнившись их красотой, когда писал RTOS "для себя". Чисто из научного интереса.

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

Как нибудь поподробней можете рассказать про свою реализацию?
Сколько задач было? Какое время цикла?

Ага понятно. Дайте определение монолитной задачи или укажите где про это можно почитать.

Все-таки не стоит мешать эти вещи. Потому, что тут очень разные требования к обеспечению надежности и соответственно решения.

Также есть разница по

Тут опять же разные требования и разные решения обеспечения надежности.

Да не слушайте вы их.
Для круто надежных разработок есть такой стандарт DO-178B.

Он обходится без чудотворных монолитных задач.

Когда 7 лет назад я работал в компании, которая для авиации делала программы, было только две операционки, которые сертифицированы под это. QNX не была к моему удивлению.
Rate Monotonic Scheduling никак операционку не заменит. Он просто отвечает на вопрос как правильно (и возможно ли) расставить приоритеты задачам, чтобы критические задачи не опаздывали. До формализации этого алгоритма делали так: ставили как подскажет интуиция, а когда выяснялось, что есть проблемы, то исправляли. Я сделал можество устройств, некоторые можно купить на ebay и у меня ни разу не возникало проблем с приоритетами.