Przejdź do treści

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 for i 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

  1. Dwie subskrypcje istnieją przed publikacją 1 i 2.
  2. Obie odczytują 2; wartość 1 została zastąpiona przed obserwacją.
  3. Ponowny odczyt tej samej subskrypcji bez publikacji nie daje nowego zdarzenia.
  4. Po publikacji 3 powstaje nowa subskrypcja. Nie otrzymuje historycznej publikacji 3.
  5. 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 recv i for do 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. Oczekiwana diagnostyka: E0047.

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 for po 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 for po stream odczytuje Latest() 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.