sea

Quelea — a declarative programming model for eventually consistent data stores

The store is a collection of replicas, each storing a set of objects (x, y, . . .) of a replicated data type. For the sake of an example, let x and y represent objects of an increment-only counter replicated data type (RDT) that admits inc and read operations.

We say that the effects inc1x and inc2x are visible to the effect (inc4x) of x.inc, written logically as vis(inc1x, inc4x) ∧ vis(inc2x, inc4x).

To capture happens-before, we define an irreflexive transitive session order relation that relates the effects of operations arising from the same session. For example, in Fig. 1, inc4x and inc5x are in session order (written logically as so(inc4x, inc5x)).

same object session order (soo = so ∩ sameobj)
same object happens-before order (hbo = (soo ∪ vis)+)
happens-before order (hb = (so ∪ vis)+)

Causal Visibility (CV) ::= ∀a, b, c. hbo(a, b) ∧ vis(b, c) ⇒ vis(a, c) 
Causal Consistency (CC) ::= ∀a, b, c. hbo(a, b) ⇒ vis(a, b)
Strong Consistency (SC) ::= ∀a, b. sameobj(a, b) ⇒ vis(a, b) ∨ vis(b, c)

Read Your Writes (RYW) ::= ∀a,b. soo(a, b) ⇒ vis(a, b)
Monotonic Reads (MR) ::= ∀a,b,c. vis(a, b) ∧ soo(b, c) ⇒ vis(a, c)
Monotonic Writes (MW) ::= ∀a,b,c. soo(a, b) ∧ vis(b, c) ⇒ vis(a, c)
Writes Follow Reads (WFR) ::= ∀a,b,c,d. vis(a,b)∧vis(c,d)∧(soo ∪ =)(b,c) ⇒ vis(a,d)

∀a,b,c.txn{a,b}{c} ∧ sameobj(a,b) ∧ vis(a,c)⇒vis(b,c)
∀a,b,c.txn{a}{b,c} ∧ sameobj(b,c) ∧ vis(b,a)⇒vis(c,a)

∀(a, b : getBalance),
 (c : withdraw ∨ deposit),
 (d : withdraw ∨ deposit). txn{a,b}{c,d} ∧ vis(c,a) ∧ sameobj(d,b)⇒vis(d,b)
∀a,b,c,d.txn{a,b}{c,d} ∧ so(a,b) ∧ vis(c,a) ∧ sameobj(d,b)⇒vis(d,b)
∀a,b,c,d.txn{a,b}{c,d} ∧ vis(c,a) ∧ sameobj(d,b)⇒vis(d,b)


ШИВА-РАМА-КРИШНА-Н!
______________
[1]. http://kcsrk.info/papers/quelea_ieee16.pdf
KC Sivaramakrishnan, Gowtham Kaki, Suresh Jagannathan
IEEE Data Engineering Bulletin, 39(1): 52 64, March 2016
sea

N2O over MQTT + KVS



Пришла пора завернуть весь стек протоколов N2O в какой транспорт, который поддерживает, что-то более сложное чем ACK, такой транспорт — MQTT, он легковеснее AMQP, который, давайте без обид, порос кольцами уже, как и riak. Вообщем, пока emqtt.io еще позволяет, нужно быстро форкануться и повыбрасывать оттуда половину либ.

Из чего состоит EMQ — компания производитель EMQ Enterprise, Inc, автор Feng Lee. В основе лежит esockd — очередной неблокирующий сервер (типа ranch), в качестве веб сервера используется mochiweb, его же и вебсокеты.

emqtt.io — это пример как нужно писать приложения, минимальная документация, отпидерашеный код, приятно работать. Только там все на lager завязали и в итоге, чтобы залогировать нужно lager, lager_syslog, gen_logger, goldrush, syslog. Поэтому пришлось форкануть это все. Или просто выброосить, но lager в продакшине любят, так как проверен. Ладно не буду пока удалять.

Теперь о рекомендациях по общей архитектуре. Стек протоколов N2O я вижу как федерацию, аналогичную CORBA/OASIS/XMPP поверх различных транспортов. До этого — это был BERT/JSON кодировка over WS/WSS транспорт, теперь качество и количество транспортов расширилось до MQTT over WS/WSS, TCP/TLS. Т.е. появился базовый посредник, с ack+pubsub+presence+ping протоколом, соответственно N2O HEART ["PING","N2O,"] протокол уже не нужен. Такая версия N2O расширит области применения. С другой стороны дополнительное кодирование MQTT и его заголовки будут потреблять больше ресурсов.

Официальный MQTT JavaScript клиент от IBM: https://github.com/voxoz/mq/blob/master/apps/emq_dashboard/priv/www/assets/js/mqttws31.js Будем его резать и интегрировать в N2O. Есть альтернативный mqtt.js — но там как-то слишком адово как по нашим меркам. Для джаваскриптеров такое в порядке вещей считается.

MQTT как сервер приложений. Ну какие могут быть приложения у MQTT — коннектить устройства IoT. Чтобы реализовать перситенс — нужно имплементировать публичные хуки MQTT протокола:

load(Env) ->
    emqttd:hook('client.connected', fun ?MODULE:on_connected/3, [Env]),
    emqttd:hook('client.disconnected', fun ?MODULE:on_disconnected/3, [Env]),
    emqttd:hook('client.subscribe', fun ?MODULE:on_subscribe/3, [Env]),
    emqttd:hook('client.subscribe.after', fun ?MODULE:on_subscribe_after/3, [Env]),
    emqttd:hook('client.unsubscribe', fun ?MODULE:on_unsubscribe/3, [Env]),
    emqttd:hook('message.publish', fun ?MODULE:on_publish/2, [Env]),
    emqttd:hook('message.delivered', fun ?MODULE:on_delivered/3, [Env]),
    emqttd:hook('message.acked', fun ?MODULE:on_acked/3, [Env]).


Вообщем-то это все, что нужно знать людям, которые принимают решения. Инструкция для mad хипстеров не признающих rebar, mix и hex:

$ brew install erlang
$ curl -fsSL https://raw.github.com/synrc/mad/master/mad > mad \
              && chmod +x mad \
              && sudo cp /usr/local/bin
$ git clone git://github.com/voxoz/mq && cd mq
$ mad dep com rep
Configuration: [{emq_dashboard,
                    [{listeners_dash,
                         [{http,18083,[{acceptors,4},{max_clients,512}]}]}]},
                {emqttd,
                    [{listeners,
                         [{http,8083,[{acceptors,4},{max_clients,512}]}]},
                     {sysmon,
                         [{long_gc,false},
                          {long_schedule,240},
                          {large_heap,8000000},
                          {busy_port,false},
                          {busy_dist_port,true}]},
                     {session,
                         [{upgrade_qos,off},
                          {max_inflight,32},
                          {retry_interval,20},
                          {max_awaiting_rel,100},
                          {await_rel_timeout,20},
                          {enable_stats,off}]},
                     {queue,[]},
                     {allow_anonymous,true},
                     {protocol,
                         [{max_clientid_len,1024},{max_packet_size,64000}]},
                     {acl_file,"etc/acl.conf"},
                     {plugins_etc_dir,"etc/plugins/"},
                     {plugins_loaded_file,"etc/loaded_plugins"},
                     {pubsub,
                         [{pool_size,8},{by_clientid,true},{async,true}]}]},
                {emq_modules,
                    [{modules,
                         [{emq_mod_presence,[{qos,1}]},
                          {emq_mod_subscription,[{<<"%u/%c/#">>,2}]},
                          {emq_mod_rewrite,
                              [{rewrite,"x/#","^x/y/(.+)$","z/y/$1"},
                               {rewrite,"y/+/z/#","^y/(.+)/z/(.+)$",
                                   "y/z/$2"}]}]}]},
                {kvs,
                    [{dba,store_mnesia},
                     {schema,[kvs_user,kvs_acl,kvs_feed,kvs_subscription]}]},
                {n2o,[]}]
Applications:  [kernel,stdlib,gproc,lager_syslog,pbkdf2,asn1,gen_logger,
                mnesia,compiler,inets,crypto,syntax_tools,xmerl,kvs,esockd,
                goldrush,public_key,lager,ssl,mochiweb,emqttd,mad,sh,syslog]
Erlang/OTP 19 [erts-8.2] [source] [64-bit] [smp:4:4] [async-threads:10] [hipe] [kernel-poll:false] [dtrace]

Eshell V8.2  (abort with ^G)
1> 19:17:23.670 [info] Application lager started on node nonode@nohost
19:17:23.746 [info] Application ssl started on node nonode@nohost
19:17:23.749 [info] Application mochiweb started on node nonode@nohost
starting emqttd on node 'nonode@nohost'
Nonexistent: []
emqttd ctl is starting...[ok]
emqttd hook is starting...[ok]
emqttd router is starting...[ok]
emqttd pubsub is starting...[ok]
emqttd stats is starting...[ok]
emqttd metrics is starting...[ok]
emqttd pooler is starting...[ok]
emqttd trace is starting...[ok]
emqttd client manager is starting...[ok]
emqttd session manager is starting...[ok]
emqttd session supervisor is starting...[ok]
emqttd wsclient supervisor is starting...[ok]
emqttd broker is starting...[ok]
emqttd alarm is starting...[ok]
emqttd mod supervisor is starting...[ok]
emqttd bridge supervisor is starting...[ok]
emqttd access control is starting...[ok]
emqttd system monitor is starting...[ok]
Plugins: [{mqtt_plugin,emq_auth_username,"2.1.1",
                       "Authentication with Username/Password",false},
          {mqtt_plugin,emq_dashboard,"2.1.1","EMQ Web Dashboard",false},
          {mqtt_plugin,emq_modules,"2.1.1","EMQ Modules",false},
          {mqtt_plugin,emq_persistence,"1.1.2","Synrc KVS for MQTT",false}]
Names: [emq_dashboard,emq_modules,emq_persistence,emq_auth_username]
dashboard:http listen on 0.0.0.0:18083 with 4 acceptors.
19:17:25.705 [info] started Apps: [emq_dashboard]
19:17:25.705 [info] load plugin emq_dashboard successfully
19:17:25.705 [info] Application emq_dashboard started on node nonode@nohost
Load emq_mod_presence module successfully.
Load emq_mod_subscription module successfully.
Load emq_mod_rewrite module successfully.
19:17:25.802 [info] started Apps: [emq_modules]
19:17:25.802 [info] load plugin emq_modules successfully
19:17:25.802 [info] Application emq_modules started on node nonode@nohost
19:17:25.848 [info] started Apps: [emq_persistence]
19:17:25.848 [info] load plugin emq_persistence successfully
19:17:25.849 [info] Application emq_persistence started on node nonode@nohost
19:17:25.895 [warning] CLI: users is overidden by {emq_auth_username,cli}
19:17:25.895 [info] started Apps: [emq_auth_username]
19:17:25.895 [info] load plugin emq_auth_username successfully
19:17:25.895 [info] Application emq_auth_username started on node nonode@nohost
mqtt:ws listen on 0.0.0.0:8083 with 4 acceptors.
emqttd 2.1.1 is running now
19:17:25.897 [info] Application emqttd started on node nonode@nohost
19:17:25.904 [info] Application mad started on node nonode@nohost
19:17:25.957 [info] Application sh started on node nonode@nohost
19:17:26.043 [info] Application syslog started on node nonode@nohost


Open http://127.0.0.1:18083/#/websocket with admin:public credentials, Press Connect, Subscribe, Send and observe statistics http://127.0.0.1:18083/#/overview.





sea

Compiling to Categories

Ok, here's my equation for the solver, written in plain Haskell:

equation :: (Num a, Ord a) => a -> a -> Bool
equation x y =
    x < y &&
    y < 100 &&
    0 <= x - 3 + 7 * y &&
    (x == y || y + 20 == x + 30)


Here's how I run the solver:

    res <- evalZ3With Nothing opts $ do
        x <- mkFreshIntVar "x"
        y <- mkFreshIntVar "y"
        PrimE ast <-
            runKleisli (runZ3Cat (ccc @Z3Cat (uncurry (equation @Int))))
                       (PairE (PrimE x) (PrimE y))
        assertShow ast
        -- check and get solution
        fmap snd $ withModel $ \m ->
            catMaybes <$> mapM (evalInt m) [x, y]
    case res of
        Nothing  -> error "No solution found."
        Just sol -> do
            putStrLn $ "Solution: " ++ show sol


And here's the result, which also show you the equation we submitted to Z3:

(let ((a!1 (ite (<= 0 (+ (- x!0 3) (* 7 y!1)))
                (ite (= x!0 y!1) true (= (+ y!1 20) (+ x!0 30)))
                false)))
  (ite (< x!0 y!1) (ite (< y!1 100) a!1 false) false))

Solution: [-8,2]


Now with one function, I have either a predicate that I can use in Haskell code, or an input to Z3 for finding possible arguments for which it is true!
</pre>

______________
[1]. https://github.com/conal/concat/issues/4
[2]. http://conal.net/papers/compiling-to-categories/compiling-to-categories.pdf
sea

Пронумеруем типы и их значения

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

encode (X: Type) -> Nat
decode (X: Nat) -> (Sig: Type, Values: Stream Sig)


Еще это можно назвать — глобальное управление контекстами. Функция decode — может состоять из генератора Values: Nat -> Sig, который аллоцирует в виртуальной машине уникальный инстанс типа Sig по заданному Nat. Таким образом каждая возможная переменная в пространстве типов и термов на всех уровнях может индексироваться тройков Nat значений (Nat,Nat,Nat) — индекс вселенной, индекс типа, и индекс инстанса.

Конструирование термов в зависимом тайпчекере:

0 — UNIT      =
1 — NORM      = Nat      // normalisation
2 — SUBST     = Nat      // substitution 
3 — STAR      = Nat      // universe        
4 — REC       = Nat      // Cons: A -> List A -> List A
5 — VAR       = Nat Nat  // Nat, Bool, List A, Vec Nat A
6 — OR        = Nat Nat  // data
7 — AND       = Nat Nat  // record
8 — EQ        = Nat Nat  // definition 
9 — PI        = Nat Nat Nat
A — FUN       = Nat Nat Nat
B — TYPECHECK = Nat        


Пример:

encode "List A = Nil: List A | Cons: A -> List A -> List A"

0 — UNIT        // "A"
1 — UNIT        // "Nil"
2 — UNIT        // "Cons"
3 — UNIT        // "List"
4 — VAR 0 _     // A
5 — VAR 3 4     // List A
6 — REC 5       // Rec List A
7 — AND 4 6     // (A, Rec List A)
8 — VAR 2 7     // Cons: A -> List A
9 — VAR 1 _     // Nil:
A — OR 9 8      // Nil: | Cons:
B — EQ 5 A      // List A = Nil: List A | Cons: A -> List A -> List A


— основные конструкторы, которые индексируют (кроме Unit), некоторую переменную в таблице имен (индексы де Брейна), значение которой составляет тройка, таким образом словарь контекстов — List (Nat, (Nat, Nat, Nat)) — закодирован списком пар.

Для сравнения, List A в формате Lean:

1 — NS 0 u
2 — NS 0 list
3 — NS 0 α
1 — UP 1
0 — ES 1
1 — EP BD 3 0 0
4 — NS 2 nil
2 — EC 2 1
3 — EV 0
4 — EA 2 3
5 — EP BD 3 0 4
5 — NS 2 cons
6 — NS 0 a
6 — EV 1
7 — EA 2 6
8 — EV 2
9 — EA 2 8
A — EP BD 6 7 9
B — EP BD 6 3 10
C — EP BI 3 0 11
D — IND 1 2 1 2 4 5 5 12 1
sea

Семинары в НАН

Ужасный звук + украинский язык = Категорная Семантика Индуктивных типов

sea

N2O is Ditry Erlang

Запомните и никогда не делайте такого, как говорят кому дхарма, а кому карма. Поверьте, чувак который заходит на gitter, а не берет трубку телефона и набирает — не наш клиент :-) Никто такие проекты в Synrc никогда не брал и брать не будет. Ни мы, ни компании никогда не реагируем, на такую хуйню, чтобы вы не писали про нас в интернете :-)

Если мы захотим рекламную компанию дать по N2O, а мы еще этого не делали, то вы обязательно узанете. Посты на Хабре и англоязычных сайтах пишутся сами собой:

http://rgrinberg.com/posts/omegle-n2o/
http://qiita.com/dseg/items/4f2c8b04aec35cc504f0
https://kukuruku.co/post/n2o-erlang-web-framework/

Мне достаточно сказать, что на N2O написано что-то там в банках, из которых выгнали Костюшкина, и все вопросы сразу отпадут сами собой.



Кароче, вы реально считаете, что N2O запилили имаджборду и ничего не продумали насчет черного пиара? Да это же только повод, для написания вот таких постов. Главное причина то в чем? — Code Style! Шабат пацаны.

$ cd n2o/src
$ cloc .
Erlang    1199
sea

Кто-то рассказывал, что Standard ML мертв

sea

Новый сайтик на старом домене

Так как пост получил резонанс, решил обрамить немногим текстом и убрать провокативный наброс на все на свете, а то у некоторых, горячо любящих джаваскриптовую лапшу в виде TypeScript и С# и прочих любителей Гугла возникло желание разбить монитор :-)

http://semantic.vision

Домен спиздил у denis_poltavets :-) Зато подарил дизайн!
sea

Рекомендации от Mad Advisors Corp



Куда ИНВЕСТИРОВАТЬ, что НАСЛЕДОВАТЬ или ВОРОВАТЬ, на что ориентироваться:

Binary Protocols and Protocol Stacks (CORBA and SOAP Replacement)

— WebSocket
— SVG
— MQTT
— N2O
— ASN.1

Storage Systems (CODASYL and MUMPS Replacement)

— Aerospike (SSD)
— BlazingDB (GPU)
— PumpkinDB (FORTH, AVX) — лучший хакатон стартап на расте, авансом

Array Processing Languages (Fortran replacement)

— Futhark (GPU)
— Julia (AVX)
— AutumnAI (ML)

Concurrency Runtime and Languages (Ada Replacement):

— Pony (Runtime+Language, Erlang replacement, Zero Copy, CAS)
— Erlang, LING (Runtime+Language, Poor man)
— Rust (Language, Zero Copy)

R&D Languages (AUTOMATH replacement):

— Coq
— Z3
— Lean
— F*

Target Languages / Platforms for Runtime (Pascal Replacement):

— OCaml
— LLVM/MIR
— Rust
— D
— GHC

New Markets (Inexistant satisfaction) — озеро, где живут Синие Птицы и Черные Лебеди:

— VHDL FPGA toolchain replacement
— SIP/VoIP/RTP replacement
— Xen, Hyper-V, EXSI replacement
— Wolfram Mathematica replacement
— Lisp Machine replacement
— seL4 replacement

Куда НЕ ИНВЕСТИРОВАТЬ, от чего УБЕГАТЬ или что СОЗЕРЦАТЬ:

— JSON, XML, MessagePack, Text Protocols, ...
— HTML, Virtual DOM, React, Angular, Literally Any JavaScript Framework ...
— HTTP 1, 2, 3, 4, ...
C-Style Languages: Go, C, C++, JavaScript, TypeScript, ES6, ASM.JS, ...
Any LISP: Clojure, Common Lisp, Smalltalk, Self, Io, ...
Big VMs: JVM, CLR, ...
Просто унылое говно: Go, C#, Java, PHP, Scala, Python, PHP, Ruby, Elixir, Perl, node.js ...
Any RDBMS: SQL, MySQL, PostgreSQL, Oracle, ...
British Languages: Haskell, Agda, Idris, ...
APL Languages: K, J, Q, APL, ...
Almost any DHT: Riak, Cassandra, Spark, Hadoop, RethinkDB, CouchDB, Memcache, BDB, Tokio, MongoDB, Redis, ArangoDB, Neo4j, AllegroGraph, OrientDB, OrientDB
Almost any serializers: gRPC, Protobuf, Thrift, ...
Modern way of devops: Kubernetes, Docker, ...
Any product built by Google: Go, TensorFlow, Android, Blockly, Dart, Polymer,
Big Operaing Systems: UNIX, BSD, Linux, Windows, Mac

Список Обновляется. Коментарии Пендинг. Дискас.

Ты выше ЖЖ и не хочешь оставлять контент? Будь Анонимным!
Есть альтернативный канал комментирования https://erlach.co/pr/77c

Follow Back:

http://nponeccop.livejournal.com/556778.html
sea

Aerospike

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

1. Aerospike is fully open source written in C, and we can use it raw (although we don't really need it)

2. Official Erlang aerospike is a limited and not full featured. e.g. http://www.aerospike.com/download/client/erlang/2.1.2/ "Please note Erlang client only works with server 3.9.1 and older." while the current version is 3.12.1

3. Aerospike is really fast as it claims, here is most stressful test of database and most skilled guy is the world, he did analyze the aerospike for Stripe payment startup https://aphyr.com/posts/324-jepsen-aerospike

4. The nice thing is that if we are not using update/deletes, only non-removable writes and get could use aerospike even for payment processing (no write loss) — that is really fantastic http://www.aerospike.com/blog/intel-optanetm-ssds-aerospike-database-new-level-fast-operational-stores-hybrid-transactionalanalytical-processing/

5. Aerospike supports FusionIO SSD cards and latest Intel SSD which mean we are ready for the future clouds and latest technology available on the market. https://habrahabr.ru/post/155627/ https://itpeernetwork.intel.com/reaching-one-million-database-transactions-per-second-aerospike-intel-ssd/



According to the new Optane SSD product brief, the P4800X drive performs five to eight times faster than Intel's flash-based DC P3700 in internal tests at low queue depths using a mixed workload. Intel claimed the P4800X can reach as much as 500,000 IOPS -- or approximately 2 GBps -- at a queue depth of 11.

Intel said the Optane P4800X add-in card lists at $1,520 at a capacity point of 375 GB, or $4.05 per gigabyte.


6. The problem 2 could be solvable with 3-rd parties https://github.com/EnvisionX/erlang-aerospike libraries, EnvisionX is AD provider, so it seems they know what they are doing. Need to investigate deeply the quality of the code. Maybe we will need to write a simpler version for our backed team under Synrc umbrella. Already started a preparations to KVS unification library

7. Aerospike is using LuaJIT for stored procedures which explain the low latency numbers. As LuaJIT is the fastest JIT runtime in the world comparable or better that Java HotSpot in which Oracle invested millions of dollars :-)

8. Aerospike itself could be managed to power the Pub-Sub core messaging platform. Which means it is possible to use it directly with N2O without backed EMQTT orchestration. I'm thinking about reducing the complexity and cost of the solution.

От себя добавлю пару ссылок, для тек кому весь этот консалтинг до пизды, и им показуй код сука:

https://github.com/aerospike/aerospike-server/tree/master/as/src/storage/{drv_kv,drv_ssd,*}.c
https://github.com/aerospike/aerospike-server/tree/master/as/src/fabric/{paxos,*}.c
https://github.com/aerospike/aerospike-server/tree/master/as/src/base/{bin,index,scan,*}.c

Эй вы, на галерке, говнотрейдеры из Линкса, берите код, выдирайте куски и переписывайте на раст! Не ебите себе мозг. Пока это лучший сторадж который я видел своими молодыми глазами, после MUMPS. Тоже самое советую сделать Рашковскому с его PumpkinDB/Forth на расте, за его комитами я слежу и то, что он делает мне очень нравится, настоящая вторая жизнь форту, и применение правильное — для управления курсорами.

________________
[1]. http://www.vldb.org/pvldb/vol9/p1389-srinivasan.pdf