Komunikacja
chan<T>, queue<T> i stream<T> opisują różne kontrakty wymiany wartości.
Typ wiadomości T oraz model komunikacji są odrębnymi częściami znaczenia.
Ten rozdział rozróżnia kontrakt języka, jego wiązanie z runtime i gwarancje transportu.
1. Składnia i reguły poprawności
communicationType
: CHAN LT typeReference GT
| QUEUE LT typeReference GT
| STREAM LT typeReference GT
;
sendStatement
: SEND expression (TO expression)? SEMICOLON?
;
receiveStatement
: (LET | VAR) IDENTIFIER ASSIGN RECV FROM? expression SEMICOLON?
;
ackStatement
: ACK expression SEMICOLON?
;
nackStatement
: NACK expression (IDENTIFIER expression)? SEMICOLON?
;
| Reguła | Wymaganie |
|---|---|
| C01 | Każdy z trzech typów komunikacyjnych wymaga typu elementu w <...>. |
| C02 | send wymaga wartości. Jeżeli występuje to, wymagany jest również cel. |
| C03 | recv wymaga źródła; from jest opcjonalnym słowem w tej postaci. |
| C04 | ack i nack wymagają wskazania wiadomości. Samo słowo kluczowe nie stanowi pełnej instrukcji. |
| C05 | ack i nack mają znaczenie potwierdzeń kolejki; poprawność ich związania z odbiorem wymaga analizy znaczenia. |
| C06 | Wartość wysyłanej wiadomości musi odpowiadać typowi elementu celu. Sam parser nie dowodzi tej zgodności. |
send wartość odnosi się do wyjścia komunikacyjnego zadania, a
send wartość to cel wskazuje cel jawnie. return wartość jest inną operacją.
nack item reason "retry" jest przyjętą postacią z uzasadnieniem. Gramatyka
zapisuje opcjonalne uzasadnienie jako IDENTIFIER expression; samo reason
nie jest tu osobnym tokenem. Reguły dozwolonych etykiet uzasadnienia wymagają doprecyzowania.
for value in source korzysta z ogólnej składni iteracji. Zachowanie iteracji
po kanale, kolejce i strumieniu nie może być określane wyłącznie na podstawie tej samej pisowni for.
Walidacja potwierdzeń
Bieżący analizator wymaga, żeby argument ACK/NACK był identyfikatorem wartości
związanej z odbiorem z queue<T>. Naruszenie tej reguły daje E0047.
Jawne let item = recv items ustanawia powiązanie użyte w poprawnych przykładach.
Zmienna iteracji for item in items nie otrzymuje obecnie tego samego uprawnienia:
sprawdzony przykład z nack item w takiej pętli jest odrzucany jako E0047.
Poprawne przykłady z ACK/NACK są przyjmowane z ostrzeżeniem R0001: te prymitywy pozostają eksperymentalne. Akceptacja z ostrzeżeniem nie oznacza stabilnego kontraktu.
2. Porównanie kontraktów
Podstawą poniższych własności jest CommunicationRuntimeContractCatalog
oraz scenariusze communication.chan, communication.queue i communication.stream
w kontrakcie semantycznym repozytorium.
| Własność | chan<T> |
queue<T> |
stream<T> |
|---|---|---|---|
| Dostarczanie | Z presją zwrotną na producenta | Co najmniej raz, z potwierdzeniem | Najnowsza wartość |
| Zachowanie producenta | Może czekać na możliwość wysłania | Kontynuuje po dodaniu wiadomości | Kontynuuje po publikacji |
| Retencja | Do konsumpcji | Do ACK | Najnowsza wartość |
| Kolejność | FIFO | FIFO w kontrakcie kolejki | Kolejność najnowszych obserwacji, bez kompletnej historii |
| Potwierdzenia | Bez osobnego ACK/NACK kolejki | ACK/NACK i tożsamość dostarczenia | Bez ACK/NACK kolejki |
| Wielu odbiorców | Nie ustanawia broadcastu | Nie ustanawia kopii dla każdego konsumenta | Niezależni subskrybenci |
3. chan: odbiór i presja zwrotna
Kanał przenosi wartości w kolejności FIFO i zachowuje je do konsumpcji. Kontrakt dopuszcza bufor ograniczonej pojemności. Gdy nie ma miejsca na kolejną wartość, producent czeka, aż odbiór umożliwi dalsze wysyłanie.
Nie jest to bezwarunkowy rendezvous: zakończenie send nie musi czekać na
zakończenie przetwarzania przez odbiorcę, jeśli wiadomość mogła wejść do bufora.
Konsumpcja wiadomości i wykonanie jej skutku domenowego to różne zdarzenia.
Ograniczenia
- Nazwa typu nie ustala jednej liczbowej pojemności bufora dla wszystkich targetów.
- FIFO dotyczy ustalonej kolejności komunikacji; nie definiuje globalnego porządku zegarowego niezależnych producentów i węzłów.
- Presja zwrotna nie gwarantuje dostarczenia po restarcie ani odtworzenia przerwanej transmisji.
- Kanał nie jest trwałym dziennikiem. Nie deklarujemy dla niego bezwarunkowego „zero loss”.
- Wielu odbiorców wspólnego kanału nie oznacza kopii każdej wiadomości dla każdego z nich.
Przypadek określony w scenariuszu zgodności
Kanał o pojemności 1 przyjmuje wartość 1. Próba wysłania 2 czeka na odbiór 1. Po zwolnieniu miejsca producent kończy wysyłanie, a następny odbiór daje 2. Ten przypadek ustala FIFO i presję zwrotną, nie odporność sieci na awarie.
4. queue: retencja do potwierdzenia
Dodanie wartości do kolejki tworzy wiadomość o tożsamości używanej przy potwierdzeniu. Odbiór nie usuwa jej automatycznie z kontraktu retencji: pozostaje do ACK. Ponowne dostarczenie może dotyczyć tej samej wiadomości z tą samą tożsamością.
- ACK potwierdza wiadomość i kończy jej retencję w kolejce.
- NACK nie potwierdza wiadomości; zachowuje ją jako kandydatkę do ponownego dostarczenia.
- „Co najmniej raz” dopuszcza duplikaty dostarczenia. Nie gwarantuje dokładnie jednego skutku.
Przypadek określony w scenariuszu zgodności
Po dodaniu 7 i 8 odbiór wskazuje 7. Kolejny odbiór bez ACK nadal wskazuje tę samą tożsamość. NACK zachowuje ją do ponowienia. W sprawdzanym scenariuszu ACK obcego identyfikatora jej nie usuwa. Dopiero ACK pierwszej wiadomości odsłania 8.
Ograniczenia
- Tożsamość jest stabilna w badanym cyklu dostarczenia; nie ustanawiamy globalnej unikalności identyfikatorów wszystkich kolejek i restartów.
- Retencja do ACK nie określa nośnika. Sam
queue<T>nie dowodzi zapisu na dysk ani przetrwania utraty zasilania. - NACK nie określa sam opóźnienia, limitu prób, kolejki błędów ani osobnego schedulera retry.
- Kontynuowanie producenta nie oznacza nieograniczonej pamięci ani gwarantowanego czasu operacji.
- Wielu konkurencyjnych konsumentów, dzierżawy wiadomości i ich odtwarzanie po przerwaniu nie są w pełni zdefiniowane przez ten ograniczony scenariusz.
- Automatyczne ACK po bloku
fori jawne ACK/NACK wymagają rozstrzygnięcia wzajemnej relacji. Nie obiecujemy, że samo zapisanie NACK wewnątrz dowolnej pętli zapobiegnie ACK.
5. stream: najnowsze wartości i subskrypcje
Publikacja ustala najnowszą wartość. Subskrypcje mają niezależną pozycję obserwacji. Jeżeli między odczytami opublikowano kilka wartości, subskrybent może otrzymać wyłącznie najnowszą. Jeden subskrybent nie konsumuje wartości za pozostałych.
Przypadek określony w scenariuszu zgodności
- Dwie subskrypcje istnieją przed publikacją 1 i 2.
- Obie odczytują 2; wartość 1 została zastąpiona przed obserwacją.
- Ponowny odczyt tej samej subskrypcji bez publikacji nie daje nowego zdarzenia.
- Po publikacji 3 powstaje nowa subskrypcja. Nie otrzymuje historycznej publikacji 3.
- Publikacja 4 jest obserwowana przez wszystkie trzy subskrypcje.
Bezpośredni odczyt najnowszej wartości i obserwacja przez subskrypcję to odrębne operacje runtime. Nie wolno utożsamiać ich reguł pierwszego odczytu.
Ograniczenia
- Stream nie gwarantuje odbioru wszystkich publikacji ani odtworzenia historii.
- „Najnowsza” odnosi się do kolejności publikacji tego obiektu, nie automatycznie do największego znacznika czasu w rozproszonym systemie.
- Pojawienie się subskrypcji po publikacji nie ustanawia prawa do odtworzenia tej publikacji.
- Pełna relacja składni
recvifordo tworzenia subskrypcji oraz ich kończenia wymaga doprecyzowania. Testy API subskrypcji nie dowodzą wszystkich tych ścieżek. - Stream nie jest zamiennikiem kolejki z potwierdzeniami ani kanału z presją zwrotną.
6. Kontrakt lokalny a granica sieciowa
Typ komunikacyjny opisuje wymagania, które realizacja powinna zachować. Wybór transportu i przekroczenie granicy targetu wymagają dodatkowego kontraktu. Sama deklaracja nie określa MQTT, gRPC, WebSocket, pojemności, ponownego łączenia ani sposobu odzyskania brakujących danych.
Nie wolno przenosić wyniku testu lokalnego runtime na wszystkie mosty sieciowe. Kolejność po reconnect, potwierdzenie przez zdalnego odbiorcę i zapis po utracie procesu wymagają osobnego dowodu.
respond i nazwy zarezerwowane
respondStatement
: RESPOND expression SEMICOLON?
;
respond ma odrębną składnię, ale pełnego przenośnego kontekstu odpowiedzi nie
wyznaczają kontrakty chan/queue/stream. Nie przedstawiamy go jako synonimu send.
Obecność tokenu broadcast w leksykonie również nie ustanawia osobnej kompletnej
instrukcji rozsyłania.
7. Sprawdzone przykłady składni
Te przykłady potwierdzają przyjęcie albo odrzucenie jednostki przez check.
Nie są dowodem wykonania całej ścieżki dostarczania. Wiadomość potwierdzana przez
ACK/NACK jest w przykładach związana z jawnym recv, a nie z domniemaną tożsamością liczby.
Dwa przykłady negatywne sprawdzają konkretnie błąd znaczeniowy E0047, nie tylko błąd parsera.
Przykład poprawny
task Emit() @server -> chan<Int> {
send 1
}
task Read(values: chan<Int>) @server {
let value = recv values
log(value)
}
pipeline Flow {
use Emit -> Read
}
Kontrola: przykład przyjęty przez check. Nie jest to test wykonania.
Przykład błędny
task Read(values: chan<Int>) @server { let value = recv }
Powód: Odbiór recv wymaga wyrażenia wskazującego źródło.
Kontrola: przykład odrzucony przez check; kody: P0001.
Pełny zakres weryfikacji przykładów.
Przykład: Odbiór i jawne ACK kolejki
Poprawny zapis
task Handle(items: queue<Int>) @server {
let item = recv items
log(item)
ack item
}
Kontrola: przykład przyjęty przez check. Nie jest to test wykonania.
Błędny zapis
task Wrong() @server {
ack 1
}
Powód: Poprawna składniowo instrukcja jest błędna znaczeniowo: literał 1 nie jest identyfikatorem wartości odebranej z queue
Kontrola: przykład odrzucony przez check; kody: E0047.
Pełny zakres weryfikacji przykładów.
Przykład: Wybór ACK albo NACK
Poprawny zapis
task Handle(items: queue<Int>) @server {
let item = recv items
if item < 0 {
nack item reason "negative"
} else {
ack item
}
}
Kontrola: przykład przyjęty przez check. Nie jest to test wykonania.
Błędny zapis
task Handle(items: queue<Int>) @server {
for item in items {
nack item reason "retry"
}
}
Powód: W bieżącym analizatorze zmienna iteracji for nie otrzymuje powiązania wymaganego do jawnego NACK. Ten zapis jest odrzucany przez check jako E0047. Poprawny przykład używa jawnego recv.
Kontrola: przykład odrzucony przez check; kody: E0047.
Pełny zakres weryfikacji przykładów.
Przykład: Typ stream i obserwacja wartości
Poprawny zapis
task Publish() @server -> stream<Float> {
send 21.0
}
task Observe(values: stream<Float>) @server {
let value = recv values
log(value)
}
pipeline Observations {
use Publish -> Observe
}
Kontrola: przykład przyjęty przez check. Nie jest to test wykonania.
Błędny zapis
task Publish() @server -> stream<> { send 21.0 }
Powód: stream wymaga typu elementu pomiędzy nawiasami ostrymi.
Kontrola: przykład odrzucony przez check; kody: P0001.
Pełny zakres weryfikacji przykładów.
Przykład: Jawny cel send
Poprawny zapis
task Forward(target: chan<Int>) @server {
send 1 to target
}
Kontrola: przykład przyjęty przez check. Nie jest to test wykonania.
Błędny zapis
task Forward(target: chan<Int>) @server { send 1 to }
Powód: Po to musi wystąpić wyrażenie wskazujące cel wysłania.
Kontrola: przykład odrzucony przez check; kody: P0001.
Pełny zakres weryfikacji przykładów.
8. Jawne luki
| Obszar | Nierozstrzygnięta lub niepełna reguła |
|---|---|
| Odbiór bez danych | Jednolity wynik dla pustego, zamkniętego i anulowanego źródła oraz wszystkich postaci odbioru. |
| Bufory | Deklaracja pojemności, wyczerpanie zasobów i pełne zasady wielu producentów. |
| ACK/NACK | Zakres tożsamości, obca wiadomość, ponowne ACK, wyjątki i relacja jawnego NACK do automatycznego ACK. |
| Kolejka | Trwałość, wyłączność dostarczenia wielu konsumentom, retry i kolejka błędów. |
| Stream | Jawna subskrypcja w języku, cykl jej życia oraz zgodność recv/for z kontraktem obserwacji. |
| Transport | Zachowanie po przerwaniu, odtworzenie i zachowanie gwarancji przez każdy most. |
| Typowanie | Kompletne diagnozowanie wiadomości i potwierdzeń użytych w niewłaściwym kontekście. |
Granice bieżącej implementacji — nie dodatkowe reguły języka
- Lokalne kolejki emitowane przez generatory przechowują elementy w pamięci. NACK zachowuje element; w Go i TypeScript operacja może mieć puste ciało, ponieważ odbiór wcześniej go nie usuwa. Nie oznacza to silnika opóźnionych ponowień.
- Generator Go dla
forpo kolejce dopisuje ACK na końcu iteracji. Analizator odrzuca sprawdzony NACK zmiennej tej iteracji jako E0047. Niższa warstwa generatora bez powiązania potrafi wyemitować tylko komentarz; nie jest to zachowanie poprawnie zaakceptowanego programu i nie zastępuje walidacji. - Generator Go dla
forpo stream odczytujeLatest()w pętli bez pozycji niezależnej subskrypcji. Nie jest to dowód własności „bez ponownej obserwacji tej samej publikacji”, którą testuje API subskrypcji. - Testy zgodności wykorzystują rzeczywiste lokalne API C++, Go i TypeScript. Nie wykonują testu awarii sieci, trwałego nośnika ani całej składni źródłowej ACK/NACK.
9. Źródła reguł i dowodów
| Źródło w repozytorium | Zakres |
|---|---|
grammar/JunexisLang.g4: communicationType, communicationStatement, communicationExpression |
Składnia typów i operacji. |
compiler/JunexisLang.Compiler.IR/CommunicationRuntimeContractCatalog.cs |
Kanoniczne własności chan, queue i stream. |
compiler/JunexisLang.Compiler.IR/ChanRuntimeContract.cs, QueueRuntimeContract.cs, StreamRuntimeContract.cs |
Możliwości operacji i wiązanie z API. |
conformance/semantic-scenarios.json: scenariusze communication.* |
Zakres kontraktów zgodności. |
GeneratedChanSemanticConformanceTests.cs |
FIFO i oczekiwanie producenta przy buforze o pojemności 1. |
GeneratedQueueSemanticConformanceTests.cs |
Stabilna tożsamość, retencja do ACK i ponowne dostarczenie. |
GeneratedStreamSemanticConformanceTests.cs |
Zastępowanie wartości, niezależne subskrypcje i brak history replay. |
CommunicationRuntimeContractCatalogTests.cs |
Zgodność metadanych kontraktów i wiązań platformowych. |
compiler/JunexisLang.Compiler.Core/Semantics/SemanticAnalyzer.cs: ValidateAckNack oraz testy SemanticAnalyzerTests |
E0047, powiązanie z queue i eksperymentalne R0001. |
CodeGeneratorCppQueueAckTests.cs oraz generatory Go/TypeScript/C++ |
Sposób powiązania jawnych potwierdzeń z odbiorem; dowód generowania, nie pełnego wykonania. |
Źródłowego rozdziału spec/05-communication.md nie kopiujemy bez rozróżnienia
poziomów gwarancji. Jego wcześniejsze określenia „zero loss”, trwała kolejka
oraz automatyczny ACK nie stanowią samodzielnego dowodu tych własności w każdej realizacji.