- 01
- 02
- 03
- 04
- 05
- 06
- 07
- 08
- 09
- 10
- 11
- 12
- 13
- 14
- 15
- 16
- 17
- 18
- 19
- 20
- 21
- 22
- 23
- 24
- 25
- 26
- 27
- 28
- 29
- 30
- 31
- 32
- 33
- 34
- 35
- 36
- 37
- 38
- 39
- 40
- 41
- 42
- 43
- 44
- 45
- 46
- 47
- 48
- 49
- 50
- 51
- 52
- 53
- 54
- 55
- 56
- 57
- 58
- 59
- 60
- 61
- 62
- 63
- 64
- 65
- 66
- 67
- 68
- 69
Короче, размышлял я как-то на тему того, как надо делать правильный
теорем прувер, а не питушню всякую заедушную. Вот взять тот же Metamath -
там какие-то непонятные distinct правила для хуиты, что надо какие-то там
disjoint переменные, вот тут https://groups.google.com/g/metamath/c/M2dUfFATxD8
про это подробнее сказано.
Есть вот еще Metamath zero https://github.com/digama0/mm0 и это вот кажется ближе
к тому, что мне нравится.
Например вот https://github.com/digama0/mm0/blob/master/examples/assembler.mm1
тут есть какая-то теорема про ELF хедер. Это вот определение ELF идентификатора
local def ELF_IDENT_s: string =
$ ,0x7f ': ,"E" ': ,"L" ': ,"F" ':
_x02 ': _x01 ': _x01 ': _x00 ': _x00x8 $;
и там еще какой-то такой хуйней описывается то, где там точка входа записана в заголовке,
еще separation logic есть какая-то.
Но вот если почитать спецификацию для этого mm0 языка
https://github.com/digama0/mm0/blob/master/mm0.md :
pure means that this sort does not have any term formers. It is an uninterpreted domain which may have
variables but has no constant symbols, binary operators, or anything else targeting this sort. If a sort has
this modifier, it is illegal to declare a term with this sort as the target.
strict is the "opposite" of pure: it says that the sort does not have any variable binding operators. It is illegal
to have a bound variable or dummy variable of this sort, and it cannot appear as a dependency in another
variable. For example, if x: set and ph: wff x then set must not be declared strict. (pure and strict are not
mutually exclusive, although a sort with both properties is not very useful.)
provable means that the sort is a thing that can be "proven". All formulas appearing in axioms and theorems
(between $) must have a provable sort.
free means that definitions and theorems are not allowed to use dummy variables with this sort.
то кажется мне, что слишком это сложно. Надо проще это всё сделать, по принципу какой-нибудь
хрени типа SKI кобенационного исчисления. Т.е. допустим аксиома для модус поненса
AXIOM
%A
P P $IMP %A %B
_
%B
т.е. если мы матчим некую хуйню "%A" и некую хуйню "P P $IMP %A %B" где %A и %B это некая
срань, которая может быть "что-то" "P чтото чтото" или там "P чтото P чтото чтото" и т.д.
ну короче P означает что там две какие-то хуйни, вот как в той хрени https://govnokod.ru/27420
то можем дополнительно синтезировать высказывание "%B"
А теоремы это negj композиции из аксиом и других теорем. Типы можно прикручивать через какую-то хуйню
типа если арифметику Пеано описывать, тип можно так что-то нахуевертить аксиому, ну типа
Определение что ZERO это натуральное число.
AXIOM
_
P NAT ZERO
Что если инкрементнуть натуральное, будет тоже натуральное (S это функция следования)
AXIOM
P S %A
P NAT %A
_
P NAT P S %A
В общем надо бы подумать, как там запилить максимально простой и эффективно расширяемый язык для
доказывания всякой хуйни.
Смотрел Coq - какая-то ебаная перепитушня со всякими там типами-хуипами и какими-то
блядь рекурсиями. Хер поймешь, как эта вся дрнсня работает. Меня ваши типы не ебут
совершенно, я хочу сам свои типы конструировать, а не полагаться на какую-то невнятную
ебанину.
Follow us!
Потому что большинство устраивают собачки в ПХП. К счастью или к сожалению.
1. Заказчикам не приходится нанимать докторов наук по кокам и хачкелям, чтобы реализовать задачу, которую может сделать школьник.
2. У технологий повышается "порог вхождения" в мир. Если ещё 40 лет назад можно было скормить ничего не подозревающему человеку assемблер и шишку, то сейчас мало кто захочет изучать что-то менее человечное, чем питон и шишарп. Чем дольше мы ждём, тем меньше интереса будет у людей к пердольной питушне.
Но специалисты понимают, что собачки кусаются, и некоторые концепции были бы полезными. А значит с течением времени в какой-то инструмент вложится очередной майкроугл. Тогда появится одно решение, рассчитанное на нормальных людей.
Не куча сделанной наполовину питушни - как вышло с языками программирования, а один хороший и интуитивно понятный продукт, для которого достаточно степени выпускника средней школы, и на его фоне куча остальной "разрозненной хуиты" для докторов, где у пакетного менеджера нет команды "удалить пакет", а для вывода на консоль надо знать теорию категорий и монады.
Нясколько понямаю, в coq хотели дать тебе няпротиворечивую систему, в которой ты ня можешь отстрелить себе ногу. Числа, логические операторы и т.п. там строятся из очень простых вещей. Да, ня поверхности выглядит сложня и страшня, но под капотом там по сути просто лямбды да их типы ^_^
А твоя версия с няксиомами -- это как няшная с её UB'ами: някаких подушек безопаснясти, только хардкор. Конпелятор ня сможет проверить, что твоя няксиоматика ня поехавшая. Тебе придётся как-то самому вручную доказывать, что новая няксиома ничего ня портит.
З.Ы. Да, в coq, нясколько я понямаю, вообще нявозможно добавить реальную няксиому. Твой пруф будет просто импнякацией при условии что эта "няксиома" верна. Сам движок ня верит в её истинность.
Нет доказательств непротиворечивости coq. Есть столько же оснований доверять непротиворечивости кем-то написанным аксиомам, как и доверять непротиворечивости coq. В самом coq доказать непротиворечивость coq невозможно, потому что вторая теорема Гёделя о неполноте.
Если формальная арифметика S непротиворечива, то в ней невыводима формула, содержательно утверждающая непротиворечивость S.
> А твоя версия с няксиомами -- это как няшная с её UB'ами: някаких подушек безопаснясти, только хардкор.
А как мне помогает coq? Если я в coq описываю некую свою хуйню, например аксиомы из theory of array https://smt2012.loria.fr/paper1.pdf
These axioms state that storing the value v into an array a at index p and subsequently reading a’s value at index q results in the value v if the indices p and q are identical. Otherwise, the write operation does not influence the result of the read operation.
Каким образом coq защитит меня, если я при переписывании этих аксиом где-нибудь ошибусь?
Т.е. тот же массив ты мог бы построить в виде списка или дерева. И ня освнове этого вывести его свойства. И тогда ты можешь ня бояться, что они записаны няправильно. Ты просто не сможешь их доказать.
Почему в данной работе они пошли в обход системы -- я ня знаю, честно.
Для этого тебе надо построить из чего-то список или дерево (или чтобы список или дерево уже было). А никаких списков и деревьев может не быть. И вообще, может лучше я сначала построю theory of array, и потом поверх нее построю списки и деревья.
Как все настоящие программисты знают, единственной полезной структурой данных является массив. Строки, списки, структуры и наборы — это все разновидности массивов и их можно рассматривать как массивы без усложнения вашего языка программирования.
Но, как мне кажется, когда ты добавляешь в свою систему какую-то новую сущность, выгоднее её выразить в терминах существующих, а ня ебашить няксиомы о ней. Меньше рисков получается.
Это, вообще говоря, не важно. Можно сделать аксиоматику для массивов с нуля, и можно параллельно сделать аксиоматику для деревьев с нуля, а потом формально доказать, что массивы вот так можно описать через деревья, и что деревья можно вот так описать через массивы. Т.е. что такие-то рассуждения в теории массивов изоморфны таким-то рассуждениям в теории деревьев, и это все тождественно.
По сути, на практике ты будешь доказывать что-то в духе изоморфизма конструкций твоего DSL'а и инструкций какого-нибудь arm'а или x86. А посрединке между ними будут всякие теории о массивах, деревьях, лямбдах и т.п. В каком из базисов ты это делаешь -- не так уж важно, их бесконечно много. Лишь бы выбранный базис не позволял доказывать хуйню на ровном месте.
А судьи кто? Как оценивать сложность? Я вот например не уверен, что теория массивов чем-то сложнее теории деревьев.
И что? Любая вычислимая функция выражается через программу на языке брейнфак, но это не значит, что любую вычислимую хрень надо сводить к брейнфаку и в неких брейнфак-аксиомах доказывать. Если ты доказываешь корректность сортировки пузырьком на языке Си, ты будешь на брейнфаке описывать некий Си-интерпретатор который запускается в брейнфаке, а потом доказывать через брейнфак-аксиоматику, что если мы в брейнфак засунем Си-интерпретатор и в Си-интерпретатор скормим такой-то код сортировки на Си, то эта сортировка будет работать как надо?
Ну не совсем так. Допустим, я построила массивы на брейнфаке (х.з. как это делать, если честно) и доказала несколько теорем о них (те самые утверждения, что ты привёл как аксиомы).
Теперь я могу эти теоремы юзать чтобы доказать что-то более интересное и высокоуровневое. Что сортировка сортирует, к примеру. И ни я ни тайпчекер не будем углубляться в детали реализации этих массивов пока не понадобится какая-то новая хитровыебанная теорема о них.
Или я могу попытаться на основе брейнфака выразить лямбда-исчисление и дальше уже пользоваться им, забыв на время о брейнфаке.
Т.е. базис -- это просто базис.
Много способов есть. Можешь переписать Coq на брейнфак и в Coq построить массивы.
Логика высказываний, пропозициональная логика или исчисление высказываний, также логика нулевого порядка — это раздел символической логики, изучающий сложные высказывания, образованные из простых, и их взаимоотношения.
Исчисление конструкций — теория типов на основе полиморфного λ-исчисление высшего порядка с зависимыми типами, разработана Тьерри Коканом и Жераром Юэ в 1986 году. Находится в высшей точке лямбда-куба Барендрегта, являясь наиболее широкой из входящих в него систем — \lambda P\omega.
Хотя, ладно, понятно почему.
§5.4
А это доказательство на самом Coq есть? Вот есть всякие примеры, когда из Coq синтезируют некоторые корректные по построению программы, кто-нибудь смог на Coq сгенерить корректный по построению Coq и его потом им же опять так пересобрать? (т.н. раскрутка компилятора)
Да, это понятно, я о том, чтобы добавить аксиом, чтобы доказать непротиворечивость того Coq, где этих аксиом нет.
Когда некие математики доказывали эту сильную нормализацию для исчисления конструкций, они опирались на какие-то аксиомы, правила вывода. Если эти аксиомы существуют, их можно записать в Coq тоже как некие аксиомы, тут я не вижу противоречия. Или эти аксиомы невыразимы в Coq? Как такое может быть?
Если рассматривать некую формальную систему "X" в которой невыводима непротиворечивость "X" но нам надо доказать ее непротиворечивость, мы создаем некую расширенную формальную систему "X++" в которой доказуема непротиворечивость "X" (но непротиворечивость "X++" уже недоказуема). Похоже что это т.н. метасистемный переход
хмм...
типа
Т.е. что если есть аксиома
то можно синтезировать аксиому
а потом еще и аксиому
и так до бесконечности. Надо чтоб метасистемный переход.
(& (& (& f a) b) c)
Будет лучше видно структуру для паттерн-нятчинга.
Ну просто у тебя уже есть скобочки, а ты унарный оператор пердолишь.
В общем это все синтаксический сахарок, который можно внешним препроцессором сделать, тащить это в базовый язык незачем.
Вот так надо, потому что "not" принимает один аргумент
- показалось
Может быть какие-то безусловные (& wff true) и (& wff false) стоит добавить чтобы можно было начать что-то строить?
А зачем тебе что-то брать? Теоремы ты строить можешь. Например транзитивность http://us.metamath.org/mpeuni/syl.html - если "из a следует b" и "из b следует c" то "из a следует c"
Никакой (& wff true) и (& wff false) не нужен.
Если @a @b @c это wff (well formed formula), мы тривиально доказываем что "& & imp @a @b" и "& & imp @a @c" это тоже wff и так можем эту теорему применить в какой-то другой теореме.
но суть, думаю, ясна
Может более явный синтаксис сделать, что у аксиом и теорем есть только одно утверждение:
Т.е. получается что какие-то элементы логики уже прям в синтаксис просочились. А мы их потом заново сочиняем.
А как определять это самое "И", если бы в теореме-аксиоме нельзя упомянуть две или более штуки?
Ну т.е.
forall a b, a -> b -> and a b
Теперь вопрос как импликацию аксиоматизировать...
Если верно а, тогда (если верно b, тогда верно and a b).
Или я туплю?
Вообще это проблема курицы и яйца.
В петухе ее элегантно решили построением и того и другого через лямбды и типы, но здесь видимо так не прокатит ;(
А j123123 какой-то ассемблер сделал или сишку с кучей &мперсандов и переводов строки. Читается как чат малолеток:
- ты как няш :*
- норм ))
- ясн ))
- а ты7
- неоч (((
- бл& (
- вще х&&во
- &здец ))
Из-за RPN что-то сложнее этой теоремки будет нячитаемо, ну да пофиг. Плюс тут надо как-то задекларировать wff и and перед использованием:
2 constructor and
1 constructor wff
А то если гуглить, это либо Росприроднадзор, либо оперативный ответвительный зажим, либо registered practical nurse, либо revenue payroll notification.
Хотя, с другой стороны, может и не надо такое гуглить, а то потом начну писать теоремы и формулы вида E=mc^2 записывать с амперсандами и скобками
Вообще говоря, в этом и идея. Ядро прувера и должно быть простым и похожим на ассемблер. А дальше поверх него уже можно наворачивать всякий сахарок и тактики без боязни обосраться.
Вот допустим
надо чтоб где-то в определении "+" было описано что оно захавывает из стека два "Nat" и "возвращает" один "Nat". И что "5" вообще нифига не захавывает, и просто является "Nat".
И если есть теорема, что "@x @x +" где @x это "Nat" можно переписать как "@x 2 *", и чтоб такую теорему применить нужным образом, если указать что "@x" это "5 5 +" то тогда питушня заматчится так
А если указать что "@x" это "5" то
Надо какой-то дополнительной питушней указывать, когда надо матчить? В общем, это немного усложняет
В префиксном формате у тебя есть точно такая же проблема (да и в инфиксном коке она тоже есть).
Допустим, мы хотим применить теорему про a + b = b + a в формуле (1 + 2) + (1 + 2). Здесь три потенциальных матча. Как указать, какой именно я хочу зареврайтить?Т.е. в любом случае надо какой-то способ для явного выбора нужного фрагмента.
надо матчить не через
а через
Или даже чтоб
И тогда в @z1 задаем
а в @z2 - нихуя.
'& & plus @c & & plus @b @a'
Кстати, а как ты это докажешь имея только если '& & plus @a @b' то '& & plus @b @a'?
Воспользуешься дополнительной леммой если '@x = @y' то '& & plus @c @x' = '& & plus @c @y'? Или как-то проще, чтобы эквивалентность не вылезала?
Ну допустим если использовать прямую польскую запись и отказаться от этих вот "&"
Имхо, тут можно попробовать доказать лемму конгруэнтности (или как там её правильно зовут): если из @a следует @b, то из plus @x @a следует plus @x @b, а так же из plus @a @y следует @b @y. Имея такие леммы можно будет легко добираться до нужных фрагментов.
Но я пока туплю, как её записать в твоей системе.
У тебя ж тут ничего ничему не равно и даже не имплицируется.
Хотя наверное можно попереставлять, потом собрать выражение с импликацией и его применить по такой-то аксиоме. Это думать надо
a+(b+c) = (a+b)+c = (b+a)+c = b+(a+c)
Но тут опять же нужна конгруэнтность плюсика (x=y -> a+x=a+y /\ x+a=y+a), чтобы можно было оперировать над кусками формулы, а не над всей целиком.
В коке она бай дизайн, насколько понимаю. А тебе её придётся доказать или принять.
http://us.metamath.org/mpeuni/ax-mp.html
Это как-то постулируется в твоей аксиоматике? Или есть какой-то пруф? Или это нужно доказать в каждом кейсе перед тем как реврайтить?
Не, ну это надо просто хуйни не делать. Если есть какая-то хуйня, где можно "перегружать" значение plus, и при такой перегрузке plus уже не складывает, а возводит в степень, и эта хуйня для перегрузки заматчилась в @z1 @z2 (как в том последнем примере) то конечно хуйня будет.
Тут надо конкретику обсуждать, придумывать непосредственно сами аксиомы и правила вывода
Пока это выглядит как деревья, состоящие из атомов (wff, and и т.п.) и конструкторов пары (&).
Над деревьями мы вводим отношение истинности. Какие-то деревья истинны, а какие-то -- нет.
Но пока у нас нет способа показать, какие из них истинны. Для этого мы вводим аксиомы, которые в простейшем случае могут сказать, что какое-то конкретное дерево истинно.
Но работать над конкретными деревьями скучно, поэтому мы вводим собачки-переменные (ака forall) чтобы составлять более интересные аксиомы, которые гласят "такое дерево истинно для любых поддеревьев @a".
И затем мы вводим ещё более сложные аксиомы, в которых есть набор входных условий: "если все вот эти деревья истинны для поддерева @a, то вот такое дерево тоже истинно для этого @a".
Поправь меня, если я написала хуйню.
З.Ы. Т.е., насколько я понимаю, пока что мы можем применять теоремы только от корня, ко всему дереву целиком. Права на работу с поддеревьями у нас пока нету.
Тут изначально нет никакой "истинности". Тут речь о выводимости т.е. можем ли мы такую-то штуку сконструировать, пользуясь такими-то аксиомами и/или уже доказанными теоремами. Если можем, то теперь эта штука - еще одна теорема, которой можно пользоваться для доказывания чего-то там.
Что-то мне подсказывает, что этот "&" тоже можно обычным термом считать, никакого особого статуса ему можно не давать (хотя может это где-то что-то ломает, но пока это неочевидно). И тогда никаких деревьев тут по-сути нет, просто списки хреней, которые матчатся какой-то хреню и если заматчились то генерируем что-то там.
Это же sed (=^ ◡ ^=)
Да в общем-то его тогда и выкинуть можно, записывая "& & and" как "and". Вроде тоже ничего не сломается.
wff @a -> wff not @a
wff @a -> wff @b -> wff and @a @b
То хуёвую формулу из них ну никак не слепить, насколько я понимаю. Можно даже попробовать это пруфнуть.
& разве что для каррирования мог бы пригодиться. Типа "& and @a" -- это унарная хуйня, принимающая bool. Другой пользы я пока не вижу.
которая через какие-то теоремы переписывается по частям
В пруверах про такое обычно не парятся... ну да ладно.
У тебя там всё равно end есть. Так что можно как-то так зареврайтить:
add_many end_add_many -> 0
add_many @a -> add @a add_many (в этом правиле @a должно быть wff)
add_many @a @b @c end_add_many ->
add @a add_many @b @c end_add_many ->
add @a add @b add_many @c end_add_many ->
add @a add @b add @c add_many end_add_many ->
add @a add @b add @c 0
Не преумняжай сущнясти. Все функции принимают на вход только один аргумент, а с зависимыми типами можно намутить, что при каррированяи тип возвращаемой лямды будет отличаться в зависимости от предыдущих аргументов.
Угу, можно вообще список сделать и fold для него запилить.
Да почему? Обычный product type. Хотя такое обычно туплом называют, конечно, а не списком.
Я думаю пока можно без него попробовать. Добавить всегда можно будет.
"Ложность" ака "невыводимость" можно будет доказать перебрав все правила и показав, что они не помогают построить такое дерево, к примеру.
К слову, пока это очень похоже на индуктивные типы в coq. Просто тип пока один: "constructible" или как ты там его назовёшь.
(1 + 2) + (1 + 2) обеспечивает кучу вариантов
1. левая замена
2. средняя замена
3. правая замена
4. 1/2/3 и левая/средняя/правая замена где угодно
5. 1/2/3 и левая/средняя/правая замена там, где ещё не заменяли
6. одновременная замена 2 выражений
7. одновременная замена 3 выражений
Дальше строим кучу разных операторов
1. замена с памятью/без памяти (с памятью убеждается, что создаются уникальные идентификаторы, а не совпадающие - x->x1 vs x->x)
2. вилка: замена без памяти, удлиняющая выражение (например, x -> x+x)
3. сход: замена, сокращающая выражение (например, x+x -> x)
4. итерация до достижения неподвижной точки
Дальше определяем числа, скажем, как
0. левая замена
1. правая
2. левая, затем правая
3. правая, затем правая
(или ещё как-то красиво)
Потом ещё находим выражения, на которых так определённые числа можно посчитать.
Да, ты можешь построить например брейнфак.
сначала идет код программы типа последовательности из "< > + - . [ ]" и там еще будет маркер "^" который означает текущий instruction pointer.
Потом разделитель "#" и дальше будет счетчик для квадратных скобок "[ ]" чтобы находить пару.
Потом опять разделитель "#" и будет как бесконечное поле из чисел от 0 до 255 с маркером, которое нулями слева и справа дописывается
Потом опять разделитель "#" и будет стандартный вывод
например если программа "+ + . > > [ > > ]" то начальное состояние будет
грустно
Та же задача о рюкзаке из простого алгоритма превращается в пердолинг с пожиранием памяти.
Вот например: когда вы делаете malloc, глибц растит вам секцию кучи (делает brk). Но если вы делаете ОЧЕ большой маллок (выше M_MMAP_THRESHOLD, mallopt(3)) то маллок делает вам анянянямный ммап.
Такие отдельные секции удобнее выпёздывать на мороз по мере их освобождения (а усекновение секции кучи можно делать только с жопы), зато анянямные секции обязаны были выравнены по страничкам
тут мы сначала видим sbrk, а потом mmap (в strace)
в /proc/<pid>/maps мы видим сначала растущий [heap], а потом анонимный регион
но оно там делает дырку
хип кончается на 01e9f000 (32108544)
анонимн регион начина на 7f4ef327b000(139977063641088)
довольно дохуя, не?
(хорошо на x64 жить)
Если все большие аллокации уходят няверх -- наверное норм.
мне вот интересно, нахуя вообще это всё? брк, хип, указатели на code и data, которые там реально в mm_struct..
Почему нельзя было просто поддержать какое-то количество регионов с разными пермишеннами, и всё?
Зачем ядру вообще что-то знать про хип-хуип?
В пинде же вроде VirtualAlloc просто создает какую-то запись VAD, и течет
А уже поверх можно создавать хипы (причем дохуя хипов)
Во всяком случае в классическом System V хак с mmapом не использовали, про него Морис не пишет.
Но БЗД уже тоже да, причем опёнок по другой причине
Old implementations were all sbrk(2) based. In OpenBSD 3.8, Thierry Deval rewrote malloc to use the mmap(2) system call, making the page addresses returned by malloc random
>можно и полностью в юзермоде эмулировать
Ну вот наскока я понимаю, виндовый ``CreateHeap`` так примерно и делает.
Правда vmmap каким-то чудом знает, какой регион (кстати, как он правильно называется у винды? address range?) это хип
https://tr1.cbsistatic.com/hub/i/2010/01/06/7fab9293-c3b4-11e2-bc00-02911874f8c8/Jan-2010-WSTips20f5-Post2FigA.jpg
вон скока хипов, причем один еще и шарбл
Да поди знает где табличку хипов подсмотреть. Виндбг так то тоже её тоже читать умеет.
Было бы круто добавить в сишку такую API: malloc с как-бы ареной. Но не вручную её создавать, а делегатить операционке
(В glibc есть арена, но она не про то)
В пинде есть еще анклав какой-то..
Кстати, проверил: malloc на пинде срёт в heap (увеличивая его до неебических размеров), а явный VirtualAlloc создает "private" (ну или какую закажешь) address range.
Ренджи на пинде можно еще смотреть через kernel debugger: У !process (который показывает EPROCESS) есть поле "VDA root", которое адрес корня бинарного дерева, где хранятся VDA (у прыщей вроде есть еще linked list к дереву, а у NT только дерево), и потом по !vda можно его смотреть.
К сожалению, у меня нет пинды с поддержкой kernel debug, шоб проверить
зы: у обычного процесса еще можно посмотреть свои мапы через ``VirtualQuery``
на линуксе есть анонимный ``mmap``, на windows есть ``CreateHeap``: они создают отдельные регионы памяти, которые потом можно целиком анмапнуть или удалить
Именно поэтому я за контроллеры.
Так mmap в линуксе это сискол, а CreateHeap это какая-то винапи-хуитень. Тебе наверное надо NtAllocateVirtualMemory
Или NtAllocateUserPhysicalPages
Зачем они столько хуйни в винде понаделали?
NtAllocateUserPhysicalPages
NtAllocateUserPhysicalPagesEx
NtAllocateVirtualMemory
NtAllocateVirtualMemoryEx
NtFlushVirtualMemory
NtFreeVirtualMemory
NtFreeUserPhysicalPages
NtLockVirtualMemory
NtProtectVirtualMemory
NtQueryVirtualMemory
NtReadVirtualMemory
Сколько же хуйни
Зачем -- это вопрос к Дэвиду Катлеру, но работает именно так.
В линуксе новый регион создается через mmap (ну или shmget), а в винде через VirtualAlloc.
Но CreateHeap более высокоуровневый, позволяет не думать про конкретные VDA, их мапинг на страницы итд
На сей раз на прыще
``mmap`` c ``MAP_ANON | MAP_PRIVATE`` возвращает адрес, который хорошо виден в ``/proc/[pid]/map``, и регион там анонимный
``malloc``, как было сказано выше, либо увеличивает регион ``[heap]``, либо создает новый, если область памяти слишком велика.
Сравним с FreeBSD:
Анонимный ``mmap`` требует ``-1`` в качестве fd, иначе возвращает invalid arguments (прыщи работают и так).
Удобная утилита ``procstat`` (жаль, что на прыще такого нет) показывает ренджи памяти, правда пометки ``heap`` там нет: регион, как регион
Если сравнить два региона
то в аутпуте они будут рядышком, но mmap намного дальше хипа (сначала хип, потом mmap)
---
Фряша обссыкивает sbrk:
The brk() and sbrk() functions are legacy interfaces from before the ad-
vent of modern virtual memory management. They are deprecated and not
present on the arm64 or riscv architectures. The mmap(2) interface
should be used to allocate pages instead.
Traditionally, allocators have used sbrk(2) to obtain memory, which is
suboptimal for several reasons, including race conditions, increased
fragmentation, and artificial limitations on maximum usable memory. If
sbrk(2) is supported by the operating system, this allocator uses both
mmap(2) and sbrk(2), in that order of preference; otherwise only
mmap(2) is used.
Компания просит своих пользователей срочно обновить их.
Фирма по кибербезопасности Sangfor случайно опубликовала инструкцию, где говорится, как с помощью диспетчера печати Windows удаленно получить доступ к другому компьютеру. Jбновления, которые устраняют эту уязвимость, Microsoft уже выпустила.
Блин, вот реально, все сервисы от мс надо блочить нахер.
З.Ы. Причем вроде диспетчер печати в десятке уже засендбоксен был... Или не весь?
На семерке он работает от "System"
Ну и вероятно слушает RPC порт для named pipes, чо
http://joeyh.name/blog/entry/a_bitter_pill_for_Microsoft_Copilot/