Documentazione di lungo

Come chiamare operazioni asincrone dell’host

Scrivi programmi Lean che chiedono all’host di eseguire operazioni in modo asincrono, chiamali come funzioni asincrone native in ogni linguaggio e dimostra che cosa fanno rispetto a un modello.

In questa sezione

Questa guida mostra come un programma Lean chiede all’applicazione di fare qualcosa a cui risponde più tardi (leggere un database, scaricare una pagina, aspettare un utente) e prosegue con la risposta. Ogni export che restituisce un programma del genere diventa una funzione asincrona nativa in ogni linguaggio, che riceve un handler che esegue le operazioni. L’esempio è il crate async-store nella directory examples di lungo-rs: programmi su un archivio chiave-valore tenuto dall’host.

Dichiara le operazioni

Le operazioni sono i costruttori di un tipo induttivo; un’istanza di Lungo.Async.Interface dice con che cosa si risponde a ciascuna, e @[lungo_facility] ne fa una facility asincrona. Il progetto richiede la libreria Lean di lungo.

import Lungo

namespace Store

open Lungo.Async

/-- What a program asks of the store. -/
inductive StoreOp where
  | get (key : String)
  | put (key value : String)

@[lungo_facility "store.kv"]
instance storeOps : Interface StoreOp where
  Ret
    | .get _ => Option String
    | .put _ _ => Unit

Il tipo delle operazioni e le sue risposte devono passare all’host come dati (LNG0707):

  • il tipo delle operazioni è un tipo induttivo senza parametri né indici, i cui campi sono dati che un host può fornire (non dimostrazioni né tipi);
  • ciò con cui si risponde a ogni costruttore si riduce a un tipo fissato dal solo costruttore, non dai suoi campi (Ret (.get k) non può dipendere da k).

@[lungo_facility] controlla entrambe le condizioni quando viene applicato, e lungo le controlla di nuovo quando legge il programma. I costruttori sono le operazioni della facility: una facility asincrona non ha extern @[lungo_operation].

Scrivi i programmi

Un programma è un Lungo.Async.Program StoreOp α; Program.perform op chiede all’host di eseguire op e ne restituisce la risposta, in notazione do:

/-- Copies the value at `src` to `dst`; whether there was one. -/
def copy (src dst : String) : Program StoreOp Bool := do
  match ← Program.perform (StoreOp.get src) with
  | none => return false
  | some v =>
    let _ ← Program.perform (StoreOp.put dst v)
    return true

Scrivi il costruttore per intero (StoreOp.get src, non .get src) dove si fa il match sulla risposta: il tipo della risposta è noto solo quando lo è l’operazione.

Un export che restituisce Program Op α è una funzione asincrona; un programma può essere solo ciò che un export restituisce, non parte di un altro valore (LNG0707).

Chiamalo

Ogni linguaggio chiama l’export con un handler che ha un metodo per operazione, che riceve i campi del costruttore e restituisce la sua risposta, in modo asincrono. Il programma procede finché chiede un’operazione, aspetta la risposta dell’handler e riprende con essa; può chiedere un numero qualsiasi di operazioni, e un numero qualsiasi di chiamate può essere in attesa contemporaneamente, con risposte in qualsiasi ordine.

Un errore dell’handler abbandona il programma: lungo lo rilascia, e la chiamata fallisce con quell’errore. Lo stesso vale per l’annullamento della chiamata. Un programma riprende al massimo una volta per ogni operazione che chiede.

Rust

Il trait generato prende il nome dal tipo delle operazioni; ogni metodo restituisce un future, quindi lo implementa una async fn, e l’export è una async fn per qualsiasi executor:

use async_store::StoreOpHandler;

struct Memory {
    data: Mutex<HashMap<String, String>>,
}

impl StoreOpHandler for Memory {
    type Error = Unavailable;

    async fn get(&self, key: String) -> Result<Option<String>, Unavailable> {
        Ok(self.data.lock().unwrap().get(&key).cloned())
    }

    async fn put(&self, key: String, value: String) -> Result<(), Unavailable> {
        self.data.lock().unwrap().insert(key, value);
        Ok(())
    }
}

let copied: bool = async_store::copy(&memory, "a".into(), "c".into()).await?;

L’errore di un metodo è ciò che l’export restituisce. Scartare il future dell’export rilascia il programma.

Go

L’export riceve un context.Context e l’handler; anche ogni metodo riceve il contesto:

type memory struct {
	mu   sync.Mutex
	data map[string]string
}

func (m *memory) Get(ctx context.Context, key string) (lungo.Option[string], error) {
	m.mu.Lock()
	defer m.mu.Unlock()
	v, ok := m.data[key]
	return lungo.Option[string]{Value: v, Valid: ok}, nil
}

func (m *memory) Put(ctx context.Context, key, value string) (lungo.Unit, error) {
	m.mu.Lock()
	defer m.mu.Unlock()
	m.data[key] = value
	return lungo.Unit{}, nil
}

copied, err := store.Copy(ctx, m, "a", "c")

L’errore di un metodo, un panic o la fine di ctx abbandonano il programma: la chiamata restituisce l’errore (ctx.Err() quando il contesto è terminato), oppure va di nuovo in panic.

Python

L’export è una funzione coroutine; un metodo dell’handler è una coroutine o restituisce direttamente la sua risposta:

class Memory:
    def __init__(self):
        self.data = {}

    async def get(self, key):
        return self.data.get(key)

    async def put(self, key, value):
        self.data[key] = value

copied = await store.copy(Memory(), "a", "c")

Un’eccezione dell’handler viene sollevata dalla chiamata; annullare il task (asyncio.CancelledError) abbandona il programma.

Swift

L’handler è conforme a <Modulo><Op>Handler (qui StoreStoreOpHandler), un protocollo Sendable di metodi async throws; l’export è async throws:

actor Memory: StoreStoreOpHandler {
    var data: [String: String] = [:]

    func get(_ key: String) async throws -> String? { data[key] }

    func put(_ key: String, _ value: String) async throws -> LungoUnit {
        data[key] = value
        return LungoUnit()
    }
}

let copied = try await copy(Memory(), "a", "c")

Un errore dell’handler viene lanciato dalla chiamata; annullare il task lancia CancellationError.

TypeScript

Un metodo dell’handler restituisce la sua risposta o una promise di essa; l’export restituisce una promise e accetta un AbortSignal facoltativo:

const data = new Map();
const memory = {
  get: async (key) => (data.has(key) ? data.get(key) : null),
  put: async (key, value) => { data.set(key, value); return null; },
};
const p = await load();
const copied = await p.copy(memory, "a", "c", { signal: AbortSignal.timeout(5000) });

Un rifiuto dell’handler rifiuta la chiamata; l’interruzione del segnale la rifiuta con il motivo del segnale.

C

L’export restituisce il primo passo del programma; l’host risponde a ogni operazione con lungo_resume, finché il passo è LUNGO_STEP_DONE:

lungo_step step;
lungo_error *error = NULL;
if (store_copy(src, dst, &step, &error) != LUNGO_OK) { /* malformed arguments */ }
while (step.kind == LUNGO_STEP_CALL) {
    lungo_value *answer;
    if (lungo_value_ctor_index(step.value) == STORE_STORE_OP_GET) {
        answer = lookup(store_store_op_get_key(step.value)); /* an Option String */
    } else {
        write(store_store_op_put_key(step.value), store_store_op_put_value(step.value));
        answer = lungo_value_unit();
    }
    uint64_t resumption = step.resumption;
    lungo_step_clear(&step);
    int32_t status = lungo_resume(resumption, answer, &step, &error);
    lungo_value_free(answer);
    if (status != LUNGO_OK) { /* LUNGO_MALFORMED: an answer of another type */ }
}
bool copied = lungo_value_get_bool(step.value);
lungo_step_clear(&step);

step.value è l’operazione richiesta (un valore del tipo delle operazioni) o il valore del programma; la risposta è presa in prestito. Una risposta di un altro tipo viene rifiutata con LUNGO_MALFORMED e abbandona il programma; riprendere di nuovo una ripresa, o una abbandonata, dà LUNGO_STALE. Per abbandonare un programma, chiama lungo_async_cancel(step.resumption).

Conta ciò che è in attesa

Ogni linguaggio riporta quanti programmi sono in attesa di una risposta, numero che torna a zero quando ogni chiamata si è conclusa: lungo.Outstanding() in Go, lungo_py.outstanding() in Python, lungoOutstanding() in Swift, outstanding() del programma in TypeScript (ogni programma caricato ha il suo) e lungo_async_outstanding() in C. In Rust un programma in attesa è tenuto dal future che lo aspetta.

Dimostra che cosa fa un programma

Un programma è un dato, quindi Lean può eseguirlo rispetto a un modello dell’host. Program.run lo interpreta con un handler qualsiasi in una monade qualsiasi; qui un archivio è una funzione dalle chiavi ai valori, e il modello risponde in StateM:

abbrev Contents := String → Option String

private def Contents.set (contents : Contents) (key value : String) : Contents :=
  fun k => if k = key then some value else contents k

@[lungo_spec "lungo.model"]
noncomputable def Model : (op : StoreOp) → StateM Contents (Interface.Ret op)
  | .get key => fun s => (s key, s)
  | .put key value => fun s => ((), s.set key value)

@[lungo_claim "lungo.law" subject copy spec Model]
theorem copy_model (s : Contents) (src dst : String) :
    (Program.run Model (copy src dst)).run s =
      match s src with
      | none => (false, s)
      | some v => (true, s.set dst v) := by
  cases h : s src <;> simp [copy, Program.perform, Program.run, Model, h, bind, Program.bind,
    StateT.run, StateT.bind, pure, StateT.pure]

Contents.set è private: serve al modello e ai claim, e una definizione pubblica verrebbe esportata in ogni binding, dove una funzione su un tipo funzione non serve. Il claim dice che cosa fa copy a ogni archivio tenuto come lo tiene il modello. Per dire che vale per l’archivio dell’host, enuncialo come assunzione (vedi come dichiarare facility e assunzioni). Program.Admits e Program.trace mettono in relazione un programma con le operazioni che chiede e le risposte che riceve, per claim sugli scambi stessi (vedi come dichiarare claim sugli export).