PTC-20171

Projeto de Protocolos: Diário de Aula 2017-1

Professor: Marcelo Maia Sobral
Encontros: 2a feira/15:40 (Semana B), 4a feira/15:40
Atendimento paralelo: 3a de 13:00 às 14:00h, 4a de 8:30 às 9:30h

Plano de Ensino

Referências complementares

• ASN.1
• Internet Standard 68 (ABNF)
• SDL Forum
• RFC-1317: On the Design of Application Protocols
• Protocol Design Beyond Graph-Based Models
• Protocol Design (entrevista)
• Inrodução a C++ (com referências bibliográficas)

Avaliações

As avaliações são de dois tipos:

1. Projetos: feitos em equipes de até dois alunos, são desenvolvidos ao longo da disciplina. Os resultados parciais devem ser entregues por meio de relatórios parciais, e o resultado final deve ser demonstrado na prática e descrito em um relatório conclusivo.
2. Tarefas: feitas individualmente, e servem para ajustar os conceitos dos projetos (podem aumentá-los ou reduzi-los).

Aluno	Projeto 1	Projeto 2	Projeto 3	FINAL
André	9	8	9	9
Gabriel	9	8	9	9
Gustavo	8	5	8	6
Lucas	8	5	8	6
Marcos Vinicios	8	5	8	6
Maria Luiza	9	8	9	9
Tamara	8	5	8	6

Obs: D* = não fez a avaliação.

Softwares

• Compilador ASN.1
• ANTLR (Another Tool for Language Recognition)
• APG (ABNF Parser Generator)
• SPIN Model Checker

13/02: Introdução

• Caracterização de protocolos por meio de um exemplo: sintaxe, comportamento, temporização, semântica. Princípios de projeto e propriedades desejáveis de protocolos. Análise de um protocolo real.

• Projeto 1: um protocolo de comunicação
• Projeto 2: um protocolo de aplicação
• Projeto 3: implementação de um protocolo padrão segundo uma especificação

Um protocolo é uma parte muito importante de um sistema de comunicação. A comunicação de dados pode ser entendida como troca de informação entre dois dispositivos através de algum meio de comunicação. A comunicação ocorre no âmbito de um sistema de telecomunicações, composto por equipamentos (hardware) e programas (softwares). Um sistema básico de comunicação de dados se constitui de cinco componentes:

1. A mensagem: a informação a ser transmitida. O conteúdo da mensagem, seja um texto, música, video, ou qualquer outro tipo de informação, é representada por conjuntos de bits (dígitos binários).
2. Transmissor: dispositivo que transmite a mensagem.
3. Receptor: dispositivo que recebe a mensagem.
4. Meio de comunicação: caminho físico por onde viaja a mensagem do transmissor até o receptor.
5. Protocolo: conjunto de regras que governa a comunicação de dados.

Os sistemas de comunicação reais, incluídas as redes de computadores, são bem mais complexos do que esse modelo simplificado. No entanto, todos podem ser entendidos, em alguma medida, a partir desse modelo. Nesta disciplina estudam-se princípios e técnicas para projeto de protocolos, incluindo formas de verificar a consistência e correção de seu funcionamento.

Serviço e Protocolo

Um sistema de comunicação provê serviços para as aplicações ou usuários realizarem ações que envolvam a comunicação entre sistemas através de uma rede. Por exemplo, existem serviços para transferência de arquivos, reprodução remota de videos e músicas, execução remota de programas, pesquisa por informação, e muitos outros. O conceito de serviço está relacionado ao de protocolo. Um serviço é provido por entidades que interagem de acordo com um protocolo. Assim, um serviço é um dos elementos envolvidos na especificação de um protocolo. As figuras a seguir mostram a relação entre esses conceitos, primeiro apresentando somente a visão de um serviço para um usuário, e, em seguida, a relação entre serviço e protocolo.

Um serviço visto por um usuário

O serviço provido pelo protocolo

Protocolos reais

Que protocolos existentes despertam suas curiosidades sobre os detalhes de seus projetos ? Identifiquem alguns protocolos, e anotem suas finalidades e características.

Protocolo	Finalidade	Características
NTP	Sincronizar os relógios dos computadores ligados a rede.	Utiliza uma versão do algoritmo de Marzullo para determinar o tempo dos servidores corrigindo os efeitos da variação da latência da rede. Utiliza uma hierarquia mestre-escravo onde o servidor envia o horário UTC aos equipamentos da rede, enviando as informações por UDP.
HTTP	Acessar páginas web(arquivos .html na internet) através de um endereço(URL)	Permite persistência de dados ou não; mensagens são de 2 tipos(request e response); mensagens sempre tem um cabeçalho e o seu corpo é opcional; seu corpo(body) e informação útil podem ser de texto normal ou encapsuladas; o modo de comunicação é cliente-servidor; mensagens request são determinadas pelo método HTTP usado (GET, POST ...); mensagens response são determinadas pelo código de estado retornado (200, 401, 500...)
FTP	Transferência de arquivos entre máquinas em uma rede TCP/IP	Apresenta uma interface para realizar a transferência. Permite a independência entre os sistemas de arquivos de ambas as máquinas (cliente e servidor). Utiliza dois canais para comunicação: um para controle (conexão persistente) e outro para dados (conexão não persistente).
HDLC	Comunicação na camada de enlace	Orientado a bit; Orientado a conexão; modo de operação síncrono; Transmissão half-duplex e full-duplex; Transmissão através de Frames.
SIP	Utiliza o modelo “requisição-resposta”, para iniciar sessões de comunicação interativa entre utilizadores	Baseado na tecnologia HTTP, o SIP permite a integração de vários conteúdos. Reúne a tecnologia que permite a transmissão de dados em várias meios de comunicação virtual, contando com a velocidade e mobilidade da rede VoIP.

Análise dos protocolos

De acordo com Gerard Holzmann, no capítulo 2 de seu livro Design and Validation of Computer Protocols, um protocolo é composto por cinco elementos:

1. O serviço oferecido pelo protocolo
2. As considerações sobre o ambiente em que o protocolo é executado
3. O vocabulário de mensagens usadas para implementar o protocolo
4. A codificação (ou formato) de cada mensagem do vocabulário
5. O comportamento, definido por regras de intercâmbio responsáveis pela consistência das trocas de mensagens

Com base nesses elementos, deve-se complementar ou adequar a análise dos protocolos selecionados:

Protocolo	Serviço	Ambiente de execução	Vocabulário	Codificação	Comportamento
NTP	Sincronização dos relógios dos computadores ligados a rede.	Funciona apenas em redes locais e em ambientes de redes com e sem fio.	Dados e frames de informação.		Quando um equipamento entra na rede as trocas de mensagens para a obtenção do endereço acionam o protocolo que já sincroniza o novo equipamento com a rede, e quando não há manda dados periodicamente.
FTP	Transferência de arquivos entre máquinas em uma rede TCP/IP	Apresenta uma interface para realizar a transferência. Permite a independência entre os sistemas de arquivos de ambas as máquinas (cliente e servidor). Utiliza dois canais para comunicação: um para controle (conexão persistente) e outro para dados (conexão não persistente).	Comandos e códigos	Mensagens podem ser de dois modos: em texto ou binário. Cada mensagem inclui um identificador de 3 dígitos, que indica o comando ou código correspondente.	Cliente estabelece conexão de controle com o servidor (porta 21), enviando informações de usuário e senha e comandos para mudar diretório. Com a verificação positiva do usuário o servidor mantém a conexão de controle aberta e aguarda as solicitações de transferência. Cliente solicita um arquivo. Servidor abre uma conexão de dados com o cliente (porta 20). Após a transferência concluída a conexão é finalizada.
HDLC	Oferecer comunicação na cama de enlace, utilizando transmissões síncronas de frames e orientação a bit.	Baixa taxa de transferência e ambientes ruidosos; Utilizado por protocolos como X.25, PPP e SNA.	Frames de informação, supervisão e inumerados.	Todas as mensagens tem o mesmo formato de frame, sendo alterado apenas o campo de controle (8 bits).
HTTP	Acessar arquivos de mídia (texto, páginas, áudios, vídeos) na internet	Ambiente cliente servidor, comunicações com persistência ou não de dados	Mensagens do tipo Request ou Response	Cabeçalho sempre presente(genérico, requisição/resposta e de entidades) e corpo opcional, corpo(body) e informação útil podem ser de texto normal ou encapsuladas	Mensagens request são determinadas pelo método HTTP (GET, POST ...) e response são determinadas pelo código de estado retornado (200, 401, 500...)
PPP	estabelecer enlace de dados por linhas seriais	canal de comunicação formado por linha serial síncrona ou assíncrona	controle, dados	binária (big endian)	??

Propriedades desejáveis de um protocolo

Ainda segundo Gerard Holzmann, no capítulo 2 de seu livro Design and Validation of Computer Protocols, um protocolo possui algumas propriedades desejáveis:

• Simplicidade: um protocolo bem estruturado pode ser construído com um pequeno número de partes bem projetadas e bem entendidas.
• Modularidade: um protocolo que realiza uma função complexa pode ser construído com partes menores que interagem de maneira simples e bem definida. Cada parte menor é um protocolo leve que pode ser desenvolvido separadamente, verificado, implementado e mantido.
• Adequação: um protocolo bem formado não é incompleto, nem possui funções que nunca são de fato utilizadas. Um protocolo bem formado se limita aos recursos existentes, além de ser estável e adaptável.
• Robustez: um protocolo robusto deve funcionar bem em condições normais, e também em situações imprevistas. Ele deve conseguir lidar com cada possível sequência de ações, em todas as possíveis condições. Ele deve ter um projeto mínimo, de forma a remover considerações não essenciais que poderiam impedir sua adaptação a condições não antecipadas.
• Consistência: protocolos não devem apresentar interações que os levem a falhar, tais como deadlocks, livelocks e terminações inesperadas.

A figura a seguir mostra a arquitetura do protocolo de enlace PPP como exemplo de simplicidade e modularidade:

Robustez e consistência são aspectos comportamentais do protocolo, que envolvem portanto a dinâmica de seu funcionamento. O comportamento de um protocolo pode ser descrito de algumas formas, sendo usual utilizar diagramas. A figura a seguir apresenta o comportamento em alto-nível do protocolo PPP (mas não significa que dela se possa concluir que ele seja robusto ou consistente):

Diretrizes de projeto

No mesmo capÍtulo 2 de seu livro, Gerard Holzmann enumera dez regras de projeto de um protocolo:

1. Definição do problema: certifique-se de que o problema esteja bem definido, com a identificação de todos os critérios de projeto, requisitos e restrições antes de iniciar um projeto.
2. Definição do serviço: deve-se definir o serviço a ser realizado em cada nível de abstração antes de decidir que estruturas devem ser usadas para implementá-los (o que vem antes de como).
3. Funcionalidades externas primeiro: projete a funcionalidade externa antes da interna. Primeiro considere a solução como uma caixa-preta e decida como ela interage com seu ambiente. Depois decida como a caixa-preta pode ser organizada internamente. Provavelmente isso consiste de caixas-pretas menores que podem ser refinadas de forma similar.
4. Mantenha a simplicidade: protocolos extravagantes são mais propensos a ter bugs que protocolos simples. Eles são mais difíceis de implementar, verificar e comumente menos eficientes. Existem poucos problemas realmente complexos em projetos de protocolos. Problemas que aparentam serem complexos costumam ser problemas misturados. A tarefa dos projetistas é identificar os problemas mais simples, separá-los, e então resolvê-los individualmente.
5. Preservar independência: não conectar o que for independente, o que significa separar questões ortogonais.
6. Mantenha o projeto extensível: não introduza o que for imaterial. Não restrinja o que for irrelevante. Um bom projeto é facilmente extensível, e resolve uma classe de problemas ao invés de uma única instância.
7. Crie um protótipo: antes de implementar um projeto, crie um protótipo de alto-nível, e verifique se os critérios do projeto são atingidos.
8. Torne-o eficiente: implemente o projeto, meça seu desempenho e, se necessário, otimize-o.
9. Verifique a implementação: confira se a implementação final otimizada é equivalente ao protótipo de alto-nível que foi verificado.
10. Não pule as regras 1 a 7

TAREFA: um protocolo imaginário

Imagine um protocolo para transferência de arquivo. Esse protocolo deve prover a transferência de um arquivo entre dois computadores, de forma que o conteúdo E os atributos de um arquivo sejam devidamente copiados. Sendo assim:

1. Especifique o serviço provido pelo protocolo
2. Faça considerações sobre o ambiente de execução do protocolo (ex: o tipo de canal de comunicação usado e suas características)
3. Defina seu vocabulário, e também a codificação de mensagens a ser adotada
4. Descreva seu comportamento

Ao final, implemente esse protocolo usando seus conhecimentos sobre redes de computadores e sistemas distribuídos. OBS:

• o canal de comunicação deve ser baseado em um protocolo de transporte. Isso elimina a possibilidade de usar protocolos de aplicação, tais como HTTP (e, por consequência, implementar algo na fa forma de web service ou coisa parecida)
• o arquivo deve ser copiado sem erros, e a cópia deve apresentar o mesmo nome e atributos que o original

A entrega da especificação e do protocolo implementado deve ser feita até dia 20/02.

15/02: Projeto 1: um protocolo de comunicação

Um protocolo de comunicação está relacionado aos mecanismos necessários para a entrega de mensagens entre duas aplicações quaisquer. Considerando uma arquitetura de redes em camadas como TCP/IP, protocolos de comunicação correspondem às camadas de enlace até transporte. Questões como garantia de entrega, controle de sequência, tratamento de erros, sincronização, estabelecimento e término de sessão, multiplexação e delimitação de mensagens, entre possivelmente outras, fazem parte do projeto de tais protocolos. Para introduzir o projeto de um protocolo de comunicação, o primeiro projeto da disciplina envolve um protocolo para estabelecimento de enlace sem-fio ponto-a-ponto.

Considere o caso de uma nova interface de rede sem-fio composta por um transceiver RF capaz de transmitir a distâncias de até 1 km. No caso de distâncias como essa, a taxa de transmissão possível de ser obtida é de 2400 bps, porém distâncias menores possibilitam taxas maiores, até um máximo de 19200 bps. Esse transceiver pode ser usado como uma interface serial do tipo UART. Portanto, com ele podem-se criar enlaces de média distância e baixas taxas de transmissão.

O transceiver RF usado como UART proporciona uma camada física, cuja interface de acesso a serviço oferece operações de envio e recepção de bytes. Nenhuma facilidade para delimitação de mensagens, endereçamento, sincronização e tratamento de erros é fornecida. De fato, tais serviços devem ser implementados em um protocolo de enlace que use esse transceiver como camada física.

O projeto 1 envolve o desenvolvimento de um protocolo de comunicação usando esse transceiver RF, de forma a oferecer um serviço de comunicação com essas características.

O transceiver RF APC 220

O transceiver RF a ser utilizado se chama APC 220. Alguns documentos podem ser úteis:

• Data sheet
• Manual
• Um tutorial
• Outro tutorial

Um primeiro experimento

• A classe Serial

O primeiro contato com o transceiver RF envolve escrever um programa que transmita a mensagem Hello world! de um computador a outro usando um enlace sem-fio. Para isso, deve-se:

1. Configurar dois transceivers RF
2. Conectá-los a dois computadores diferentes usando adaptadores USB
3. Testar a comunicação usando programa para comunicação serial (ex: gtkterm, picocom, minicom). OBS: ver esta observação sobre um detalhe quanto ao uso do transceiver via USB.
4. Escrever um programa que se comunique por meio dos transceivers. Para isso podem ser úteis:
   • Serial Programming HOWTO
   • Serial Programming/Serial Linux
   • Documentação sobre termios

A serial modelada como uma classe C++

Uma implementação da classe Serial #ifndef SERIAL_H #define SERIAL_H #include <termios.h> class Serial { public: Serial(); Serial(const char * path, int rate); Serial(const Serial& orig); virtual ~Serial(); int get() { return tty_fd;} bool cca(); int write(const char * buffer, int len); int read(char * buffer, int len); int read(char * buffer, int len, bool block); char read_byte(); private: int tty_fd; }; #endif /* SERIAL_H */ serial.h #include <iostream> #include "Serial.h" using namespace std; int main() { Serial rf("/dev/ttyUSB0", B9600); string msg = "um teste ...\r\n"; char buffer[32]; int n = rf.write(msg.c_str(), msg.size()); cout << "Enviou " << n << " bytes" << endl; n = rf.read(buffer, 32); cout << "Recebeu " << n << " bytes: "; cout.write(buffer, n); cout << endl; } main.cpp: exemplo de uso da classe serial

Configuração no VirtualBox

O transceiver deve ser conectado a porta USB do computador. O Linux o reconhece e cria o arquivo de dispositivo /dev/ttyUSB0 a ele associado. Com isso a máquina virtual VirtualBox deve ser configurada da seguinte forma:

1. Habilitar a primeira porta serial (COM1)
2. O modo dessa serial deve ser Dispositivo no hospedeiro
3. O caminho do dispositivo deve ser /dev/ttyUSB0

TAREFA: início do protocolo de enlace

Implemente a delimitação de mensagens do seu protocolo de enlace, de forma que mensagens de tamanho variável possam ser transmitidas e corretamente recebidas. Essas mensagens pode ter entre 8 e 1024 bytes. Em seguida, use-as para transmitir um arquivo através do enlace sem-fio.

DICA: Ver capítulo 11 do livro "Comunicação de Dados e Redes de Computadores", de Behrouz Forouzan, ou capítulo 5 do livro "Redes de Computadores" de Andrew Tanenbaum.

22/02: Projeto 1: Sincronização e enquadramento

• Anatomia de um processo em memória no Linux: revisão sobre uso de memória e sua relação com variáveis, objetos e parâmetros em programas C/C++

A técnica de enquadramento escolhida é a do tipo sentinela. Mais especificamente, escolheu-se a versão dessa técnica implementada pelo protocolo PPP:

• Usa-se a flag 7E (01111110) como delimitador de quadros
• Usa-se um byte de escape 7D (01111101) para preenchimento de octeto
• O transmissor deve fazer pelo menos o escape dos bytes 7E e 7D que aparecerem no conteúdo do quadro
  • Cada byte que sofrer o escape deve ser modificado por meio de um XOR 20. Ex: se o byte a sofrer escape for 7E, ele deve ser modificado para 5E (7E XOR 20 = 5E).

Enquadramento (framing)

O enquadramento é uma função do protocolo de enlace responsável por delimitar quadros na interface com a camada física. Deve-se ter em mente que a camada física oferece um serviço de envio e recepção de sequências de bytes sem qualquer estrutura. Cabe à camada de enlace delimitar as unidades de dados de protocolo (PDU) dentro dessas sequências de bytes.

Existe mais de uma abordagem para delimitar quadros (ver mais no capítulo 11 de Data Communications and Computer Networks, de Behoruz Forouzan, e capítulo 5 de Redes de Computadores e a Internet, de James Kurose e Keith Ross):

Abordagem	Descrição	Exemplos
Quadros de tamanho fixo / duração definida	Quadros têm sempre mesmo comprimento ou duração	ATM, TDMA-based
Sentinela	padrão de bits/bytes delimita quadros	PPP, HDLC
Contador / duração	Cabeçalho contém duração ou comprimento do quadro	IEEE 802.11
Presença/ausência de portadora	Ausência de portadora delimita quadros	IEEE 802.11, IEEE 802.3

Atividade

1. Escolha uma abordagem viável para o protocolo de enlace a ser desenvolvido
2. Modele a abordagem usando uma máquina de estados finitos de comunicação, de forma a facilitar sua implementação. Alguns textos introdutórios sobre MEF:
   • Finite State Machines na Wikipedia
   • Finite State Machines no site Babbage's Bag
   • Cap. 8 de Design and Validation of Computer Protocols
3. Implemente a abordagem escolhida

Implementação do enquadramento

Uma máquina de estados para o receptor é esta:

Além disso, uma possível implementação dessa função do protocolo poderia ser esta:

#ifndef FRAMING_H
#define FRAMING_H

#include <cstdint>
#include "Serial.h"

class Enquadramento {
 public:
  Enquadramento(Serial & dev, int bytes_min, int bytes_max);
  ~Enquadramento();
 
  // envia o quadro apontado por buffer
  // o tamanho do quadro é dado por bytes 
  void envia(char * buffer, int bytes);
 
  // espera e recebe um quadro, armazenando-o em buffer
  // retorna o tamanho do quadro recebido
  int recebe(char * buffer);
 
 private:
  int min_bytes, max_bytes; // tamanhos mínimo e máximo de quadro
  Serial & porta;  
  char buffer[4096]; // quadros no maximo de 4 kB (hardcoded)
 
  enum Estados {Q0, Q1, Q2};
 
  // bytes recebidos pela MEF até o momento  
  int n_bytes; 
 
  // estado atual da MEF
  int estado;
 
  // aqui se implementa a máquina de estados de recepção
  // retorna true se reconheceu um quadro completo
  bool handle(char byte);
 
};

#endif

A declaração acima sugere implementar a MEF a partir do método handle da classe Enquadramento. Esse método deve ser executado para cada byte recebido, representando o tratamento de um evento pela MEF. Uma forma usual e direta de implementar uma MEF faz uso de uma estrutura do tipo switch-case. Essa abordagem se baseia em um modelo de programação estruturada. Basicamente ele depende de um algoritmo que executa um procedimento do sistema dependendo de seu estado atual e do evento. A seleção do procedimento se faz com uma estrutura switch-case. O exemplo abaixo mostra o esqueleto de uma MEF implementada usando essa técnica.

// o tratador de eventos de uma MEF hipotética
// A MEF aqui representada nada faz de útil ... 
bool Enquadramento::handle(uint8_t byte) {
  switch (estado) {
    case Q0: // estado 0
      estado = Q1; // muda para Q1
      break;
    case Q1: // estado 1
      estado = Q2; // muda para Q2
      break;
    case Q2: // estado 2
      break;
      estado = Q0; // muda para Q0
  }
}

OBS: para testar sua implementação da classe Enquadramento, use um arquivo ao invés da Serial. A transmissão de um quadro implica gravá-lo nesse arquivo. A recepção de um quadro deve ser feita pela leitura desse arquivo.

1. Experimente gravar inicialmente um único quadro, e em seguida recebê-lo.
2. Em seguida, grave dois ou mais quadros consecutivos, e depois leia-os do arquivo
3. Teste sua implementação em caso de erros de transmissão:
   1. Grave um ou dois quadros, depois escreva alguns bytes aleatórios seguidos de um novo quadro. Ao final, tente receber os quadros que foram gravados.
   2. Grave um quadro, depois grave um quadro propositalmente corrompido sem 7E ao final, depois grave um novo quadro. Receba-os e compare com o que foi gravado.
   3. Grave um quadro, depois grave um quadro propositalmente corrompido com 7D seguido de 7E, depois grave um novo quadro. Receba-os e compare com o que foi gravado.
4. Se as transmissões e recepções usando o arquivo funcionarem, experimente realizá-las usando a Serial.

OBS: este arquivo zipado contém alguns quadros de teste.

algumas coisas prontas para ajudar

#include <iostream> //#include <iomanip> #include <fstream> #include <stdio.h> #include <errno.h> #include "framing.h" using namespace std; void dump(char * buffer, int len) { int m = 0, line = 0; while (m < len) { printf("%02X: ", line*16); for (int n=0; n < 16 and m < len; n++, m++) { int x = (unsigned char)buffer[m]; printf("%02X ", x); } puts(""); line++; } } int main(int argc, char * argv[]) { string path; if (argc > 1) path = argv[1]; else path = "teste.pkt"; ifstream arq(path); if (not arq.is_open()) { perror("ao abrir arquivo de quadros "); return errno; } Enquadramento proto(arq, 8, 32); char quadro[32]; int bytes = proto.recebe(quadro); dump(quadro, bytes); } main.cpp para receber um único quadro int main(int argc, char * argv[]) { string path; if (argc > 1) path = argv[1]; else path = "teste.pkt"; ifstream arq(path); if (not arq.is_open()) { perror("ao abrir arquivo de quadros "); return errno; } Enquadramento proto(arq, 8, 32); char quadro[32]; while (true) { try { int bytes = proto.recebe(quadro); if (bytes == 0) break; dump(quadro, bytes); } catch (exception e) { cerr << "Erro ao receber quadro ! " << endl; } } } main para receber múltiplos quadros ... note que sua máquina de estados deve disparar uma exceção do tipo exception caso ocorra um erro de enquadramento int Enquadramento::recebe(char * buffer_out) { char byte; while (true) { //porta.read(&byte, 1); byte = porta.get(); // lê um byte do arquivo de teste if (porta.fail()) return 0; if (handle(byte)) { memcpy(buffer_out, buffer, n_bytes); return n_bytes; } } } método Enquadramento::recebe

01/03: Projeto 1: mecanismos básicos de um protocolo de comunicação

Um protocolo de comunicação pode incorporar um subconjunto de mecanismos elementares para que o serviço seja devidamente provido. Diferentes autores enumeram esses mecanismos, para fins de fácil compreensão. Por exemplo, Georg Holzmann no cap. 2 de Design and Validation of Computer Protocols identifica os seguintes tipos de mecanismos:

• Início e término de intercâmbio de dados
• Sincronização de transmissores e receptores
• Detecção e correção de erros de transmissão
• Formatação e codificação de dados

Mais especificamente, Controle de erros é detalhado no cap. 3 e Controle de fluxo no cap. 4.

Hartmut Konig, no cap. 5 de Protocol Engineering, 2nd ed. identifica estes mecanismos:

• Controle de erros
• Sincronização
• Gerenciamento de conexão
• Codificação e decodificação de PDU
• Ajustes em tamanhos de PDUs
• Sequenciamento
• Controle de fluxo
• Controle de taxa

Outro autor, Robin Sharp, no cap. 4 de Principles of Protocol Design, identifica estes mecanismos:

• Controle de sequência e de erros
• Controle de fluxo
• Indicação de mudança de estado do par
• Mudança de modo de serviço
• Multiplexação e separação
• Segmentação e remontagem
• Priorização

Como se pode notar, essas classificações possuem sobreposições, porém também sensíveis diferenças. Por vezes é questão de nomenclatura, em outras de ênfase em aspectos de um protocolo. No nosso caso, devemos conhecer e entender esses mecanismos para identificar quais deles são úteis para nosso protocolo de comunicação. Para realizar essa análise, antes de mais nada devemos definir o serviço a ser provido por nosso novo protocolo.

Essas funções de protocolo, para melhor entendimento e definição, devem, sempre que possível, ser relacionadas com o conceito de camadas (ver, por exemplo modelo de referência OSI). A figura a seguir resume alguns termos elementares que aparecem em um modelo em camadas (N é o número da camada), sendo eles:

• PDU: unidade de dados do protocolo (coloquialmente: pacote)
• SDU: unidade de dados de serviço (payload, carga do pacote)
• PCI: informações de controle do protocolo (cabeçalho)
• SAP: ponto de acesso a serviço (a interface ou canal para acesso à camada pelos seus usuários)

TAREFA: Definição do protocolo

Especifique seu protocolo, iniciando pelo serviço a ser oferecido. Em seguida, enumere e descreva os mecanismos a serem utilizados para implementar as funções de seu protocolo.

Serviço:

• protocolo de enlace ponto-a-ponto, para camada física do tipo UART
• encapsulamento de mensagens entre 8 e 1024 bytes
• recepção de mensagens livres de erros
• garantia de entrega
• controle de acesso ao meio
• conectado (estabelecimento de sessão)

08/03: Projeto 1: A função de controle de erros do protocolo de comunicação

• Implementação de Checksum
• Implementação de CRC em software
• Implementação do CRC-16 para PPP (RFC 1662)
• A Painless Guide to CRC Error Detection Algorithms, 3rd Edition por Ross Williams
• Um pequeno resumo sobre CRC (obtido do livro Comunicação de Dados e Redes de Computadores, de William Stallings)

O controle de erros envolve:

1. Detecção de erros: cada mensagem recebida deve ter verificada a integridade de seu conteúdo. Mensagens corrompidas devem ser rejeitadas (descartadas)
2. Recuperação de erros: mensagens descartadas devido a erros podem ser recuperadas. Existem duas abordagens:
   • Correção de erros: mensagens incluem bits de redundância que possibilita, dentro de certos limites, corrigir bits corrompidos.
   • Retransmissão: mensagens descartadas são simplesmente retransmitidas

O protocolo de comunicação a ser desenvolvido no projeto 1 deve receber apenas mensagens corretas. Para isso, pelo menos deve ser implementada uma função de detecção de erros.

Detecção de erros

A detecção de erros implica adiciona à mensagem transmitida uma certa quantidade de bits de redundância. Os valores desses bits são determinados com base no conteúdo da mensagem. Na recepção, calcula-se novamente o valor dos bits de redundância e compara-se com os bits de redundância incluídos na mensagem. Se forem iguais, presume-se que mensagem está correta.

Bits de redundância para detecção de erros

A detecção de erros envolve basicamente a escolha de uma dentre duas técnicas:

• Checksum (soma de verificação): os bits de redundância são calculados como uma soma de todos os octetos da mensagem.
• CRC (verificação de redundância cíclica): os bits de redundância são calculados usando uma forma de álgebra polinomial.

Atividade

1. Analise e escolha uma das técnicas para detecção de erros para seu protocolo.
2. Implemente a técnica escolhida.

Exemplo da classe Enquadramento com métodos para cálculo e verificação de CRC

#ifndef FRAMING_H #define FRAMING_H #include <cstdint> #include "Serial.h" class Enquadramento { public: Enquadramento(Serial & dev, int bytes_min, int bytes_max); ~Enquadramento(); // envia o quadro apontado por buffer // o tamanho do quadro é dado por bytes void envia(char * buffer, int bytes); // espera e recebe um quadro, armazenando-o em buffer // retorna o tamanho do quadro recebido int recebe(char * buffer); private: int min_bytes, max_bytes; // tamanhos mínimo e máximo de quadro Serial & porta; char buffer[4096]; // quadros no maximo de 4 kB (hardcoded) enum Estados {Q0, Q1, Q2}; // bytes recebidos pela MEF até o momento int n_bytes; // estado atual da MEF int estado; // aqui se implementa a máquina de estados de recepção // retorna true se reconheceu um quadro completo bool handle(char byte); // verifica o CRC do conteúdo contido em "buffer". Os dois últimos // bytes desse buffer contém o valor de CRC bool check_crc(char * buffer, int len); // gera o valor de CRC dos bytes contidos em buffer. O valor de CRC // é escrito em buffer[len] e buffer[len+1] void gen_crc(char * buffer, int len); // calcula o valor de CRC dos bytes contidos em "cp". // "fcs" deve ter o valor PPPINITFCS16 // O resultado é o valor de CRC (16 bits) // OBS: adaptado da RFC 1662 (enquadramento no PPP) uint16_t pppfcs16(uint16_t fcs, char * cp, int len); }; #endif

13/03: Projeto 1: Garantia de entrega no protocolo de enlace

• Seção sobre Entrega confiável no capítulo 3 do livro Redes de Computadores, 6a ed., de J. Kurose e K. Ross

A garantia de entrega pode ser definida como um serviço do protocolo que garante que uma mensagem foi entregue ao destino. Enquanto uma mensagem não tiver sua entrega assegurada, ela permanece na fila de saída mantida no transmissor pelo protocolo.

Mecanismos ARQ (Automatic Repeat reQuest) podem ser incorporados a protocolos para garantir a entrega de mensagens, preservando a ordem de envio e buscando eficiência no uso do canal. Tais mecanismos se baseiam em alguns elementos:

• Mensagens de dados
• Mensagens de confirmação positiva (ACK) e negativa (NAK)
• Numeração de sequência de mensagens
• Retransmissão de mensagens perdidas ou recusadas

Maiores detalhes podem ser lidos ndesta descrição de mecanismos ARQ, incluindo uma análise simplificada de seu desempenho.

Escolha do mecanismo ARQ a ser utilizado no protocolo de enlace

Dentre os três mecanismos ARQ elementares, pare-e-espere atende plenamente a necessidade de garantia de entrega e eficiência no uso do canal de comunicação do protocolo de enlace. Isso se conclui com a análise de utilização do canal usando pare-e-espere:

$B=9600bps$
$F=1024bytes$
$F_{ack}=4bytes$
$L=1000m$
$A_{t}={\frac {F}{B}}={\frac {1024*8}{9600}}=853ms$

$A_{tack}={\frac {F_{ack}}{B}}={\frac {4*8}{9600}}=3.33ms$

$A_{p}={\frac {L}{c}}={\frac {1000}{3\cdot 10^{8}}}=3.33us$

$U={\frac {A_{t}}{A_{t}+A_{tack}+2\cdot A_{p}}}=0.996$

Portanto, a utilização do meio seria no máximo em torno de 0.99 (ou 99%).

Modelagem do mecanismo ARQ

O mecanismo ARQ pare-e-espere deve ser modelado antes de ser implementado no protocolo. Sua disposição na estrutura do protocolo deve ser esta:

Assim, a subcamada ARQ envia e recebe quadros de dados e de confirmação da subcamada inferior (detecção de erros). O mecanismo ARQ implementado nessa subcamada pode ser modelado como duas máquinas de estado finitas: uma para transmissão e outra para recepção:

MEF para a transmissão do ARQ

MEF para a recepção do ARQ

Duas questões despontam quanto à modelagem com máquinas de estados finitos:

1. As MEF projetadas podem ser minimizadas (terem menos estados) ?
2. As MEF podem ser combinadas em uma nova MEF que contenha o comportamento tanto do transmissor quanto do receptor ?

Para investigar essas questões, devem-se estudar máquinas de estados finitos no contexto de protocolos de comunicação. MEF é uma ferramenta de modelagem útil para representar o comportamento ou regras de procedimento (proceding rules) de protocolos.

Conjunto de mensagens (vocabulário) e regras de procedimento (gramática)

O protocolo proposto no projeto 1 deve ser especificado. Isso implica sua descrição sem ambiguidades, para que possa ser corretamente implementado. A especificação envolve a definição do serviço oferecido, seu vocabulário e sintaxe, sua gramática, e a verificação de seu comportamento. Sua implementação se chama entidade de protocolo, sendo composta por software e (por vezes) hardware.

Diagrama simplificado da entidade de protocolo

A entidade de protocolo a ser desenvolvida implica pelo menos:

• Especificar e implementar a interface de acesso ao protocolo para seus usuários.
• Definir um vocabulário de mensagens, e a sintaxe abstrata dessas mensagens.
• Modelar as regras de procedimento, que determinam as sequências de mensagens e eventos aceitas pelo protocolo.
• Especificar a codificação das mensagens, o que se denomina sua sintaxe concreta.

Vocabulário

Um protocolo envolve intercâmbio de mensagens entre duas ou mais entidades. O conjunto de mensagens que compõe o protocolo é chamado de vocabulário.

Ex: um protocolo do tipo stop-and-wait possui um vocabulário dado por:

$M=\lbrace data_{0},~data_{1},~ack_{0},~ack_{1}\rbrace$

Essas mensagens podem ser usadas em sequências como mostrado neste diagrama de sequência temporal:

Cada mensagem carrega alguma informação composta por dados (o conteúdo gerado pela aplicação) e meta-dados (o conteúdo de controle gerado e usado pelo próprio protocolo). O formato das mensagens é dado pela 'sintaxe do protocolo, e existem diferentes métodos para sua descrição. Esse aspecto do protocolo deve ser trabalhado mais adiante.

Regras de procedimento

Intercâmbios de mensagens entre entidades de um protocolo devem respeitar regras quanto às sequências válidas de mensagens. O conjunto dessas regras é chamado de regras de procedimento (procedure rules).

Um protocolo é um sistema a eventos-discretos. Isso significa que as ações em um protocolo ocorrem em instantes pontuais, e não continuamente. Essas ações, ou acontecimentos, são chamadas de eventos. Por exemplo, a recepção ou envio de uma mensagem, a ocorrência de timeout, o início ou término de uma sessão são eventos ao longo de uma comunicação. Assim, um protocolo interage com seu ambiente (canal de comunicação, usuário), sendo acionado por eventos (ex: recepção de mensagem) que são respondidos com a realização de ações (ex: envio de mensagem). Seu comportamento depende do histórico de eventos passados, o que é chamado de estado. Esse tipo de sistema demanda modelos específicos para a descrição das sequências possíveis de eventos, incluindo a informação sobre o estado do protocolo.

Um diagrama de sequência temporal, como mostrado no exemplo do protocolo stop-and-wait, apesar de ilustrativo não pode ser usado para especificar as regras de um protocolo. Esse tipo de diagrama é útil para apresentar uma sequência específica de troca de mensagens, mas não todas as sequências possíveis. Quer dizer, ele não tem expressividade para especificar todas as possíveis sequências de mensagens durante as comunicações. Outros tipos de diagramas e métodos formais devem ser usados nesse caso.

Máquinas de Estados Finitos

• Capítulo 8 de Design and Validation of Computer Protocols

O protocolo stop-and-wait usado como exemplo envia uma mensagem por vez, aguardando sua confirmação para enviar uma nova mensagem. Caso a confirmação não seja recebida, a última mensagem é retransmitida. Um exemplo de protocolo que usa esse tipo de mecanismo de controle de erros é o MAC CSMA/CA do padrão IEEE 802.11. Uma versão para o stop-and-wait usa um bit para numerar mensagens, de forma a evitar a duplicação de mensagens no receptor. Assim, seu vocabulário é composto pelas mensagens msg0, msg1, ack0, ack1. As regras de procedimento desse protocolo podem ser ilustradas usando diagramas de máquinas de estados finitos, como mostrado a seguir:

Máquinas de estados finitos do transmissor para o ARQ stop-and-wait

Máquinas de estados finitos do receptor para o ARQ stop-and-wait

Uma máquina de estados finitos (ou simplesmente MEF) é composta de um conjunto de estados (as bolas) e transições (as setas). Um estado representa uma instância de comportamento do sistema (ex: ocioso, espera), e uma transição representa uma mudança de estado. Uma transição possui um estado inicial e um ou mais estados finais, além de uma condição para que ocorra (a isso se chama evento). Esse modelo básico de MEF possui expressividade para modelar alguns sistemas, e apresenta diversas propriedades importantes para analisar o comportamento desses sistemas.

Formalmente, uma MEF é definida pela tupla (Q, q0, S, T), sendo:

• Q: um conjunto não-vazio de estados
• q0: um elemento de Q denominado estado inicial
• S: um conjunto de eventos (ou mensagens), o qual forma um vocabulário
• T: uma relação de transição de estados

A relação de transição de estados T é usualmente representada por uma tabela cujas linhas contêm o estado inicial, uma ação, e o estado final. No caso da MEF do transmissor do protocolo stop-and-wait, essa tabela poderia ser:

Estado inicial	Ação	Estado final
0	envia m0	1
1	recebe ack1	2
1	recebe ack0	0
1	timeout	0
2	envia m1	3
3	recebe ack0	0
3	recebe ack1	2
3	timeout	2

Para o projeto do protocolo de comunicação, a MEF tem duas finalidades:

• Modelar as regras de procedimento do protocolo: a MEF torna possível conceber o comportamento do protocolo, definindo o que deve ser feito a depender das mensagens recebidas e transmitidas, entre outros eventos. Além disso, mecanismos internos do protocolo também podem ser modelados com MEF (ex: enquadramento).
• Verificar o comportamento do protocolo: o projeto do protocolo pode esconder problemas sutis e difíceis de identificar. Existem técnicas e ferramentas que auxiliam na verificação da correção das regras de procedimento do protocolo, evidenciando problemas tais como impasses e perdas de sincronismo.

Num primeiro momento, as MEF serão utilizadas para modelar o protocolo de comunicação. Seu uso para verificar a correção do protocolo deve ser realizado após ter sido construído um protótipo.

Atividade: MEF da garantia de entrega do protocolo de comunicação

O protocolo de comunicação deve ser modelado com uma MEF. Algumas funções do protocolo podem ser convenientemente representadas com MEF, tais como:

1. Enquadramento (framing)
2. Garantia de entrega (mecanismo ARQ)
   • Desempenho ARQ
3. Gerenciamento de conexão
4. Controle de acesso ao meio

Tendo como base a ganartia de entrega, modele-a com uma MEF. Para isso identifique os componentes da MEF capazes de representar as regras de procedimento dessa função do protocolo: estados, eventos e transições. Em seguida, faça um diagrama da MEF da garantia de entrega.

15/03: Projeto 1: Garantia de entrega no protocolo de enlace

A MEF do ARQ: N é o número de sequência de envio, e M o de recepção

A notação dos rótulos das transições da máquina de estados é:

evento / ação

... sendo evento o evento que dispara a transição, e ação as ações a serem realizadas ao final da transição.

Tanto eventos quanto ações podem conter envios e recepções de mensagens. Envios são da forma:

canal!mensagem

E recepções são assim:

canal?mensagem

... sendo que canal pode ser omitido, se o canal por onde ocorre o envio ou recepção for evidente.

22/03: Projeto 1: ARQ e integração com o sistema operacional

• Event Loop: uma técnica para tratar eventos
• Padrão de Projeto Reactor: outra técnica para tratar eventos

As sequências de processamento do protocolo

O protocolo até o momento apresenta funcionalidades elementares que o tornam capaz de estabelecer enlaces rudimentares. Dois blocos funcionais importantes foram definidos:

• Framing (enquadramento): cuida da delimitação de quadros e da detecção de erros.
• ARQ (garantia de entrega): define o formato de quadro e trata dos mecanismos para entrega e retransmissão.

A implementação desses blocos funcionais foi realizada de forma simplificada. No caso, supôs-se que as pontas de enlace se revezam entre transmissões e recepções, de forma que um lado envia um quadro e em seguida aguarda receber um quadro. Em outras palavras, o protótipo do protocolo até o momento não é capaz de reagir assincronamente aos eventos a que está sujeito em situações usuais: a qualquer instante pode-se receber um quadro ou haver a necessidade de transmitir um quadro. Para que o protocolo seja de fato funcional, nenhuma suposição pode ser feita sobre as sequências de quadros recebidas e transmitidas, tampouco as velocidade relativas das aplicações que se comunicam por meio do enlace. Isso implica repensar o modelo de sistema do protocolo para que ele possa atender esses eventos.

A busca de soluções para o protocolo inicia com uma investigação sobre as sequências de processamento que podem ocorrer. A figura a seguir identifica três sequências representativas (há algumas outras, mas essas são esclarecedoras):

Algumas sequências de processamento do protocolo

Deve-se observar que as sequências apresentadas na figura possuem diferentes origens, como se pode ver pelas setas numeradas:

• Envio: esta sequência inicia com (1) o surgimento de uma mensagem fornecida por uma aplicação. Essa mensagem deve então (2) ser encapsulada em um quadro de dados na subcamada ARQ. Ao final, o quadro gerado em ARQ (3) deve ser delimitado e transmitido pela subcamada de enquadramento.
• Recepção: esta sequência inicia com (1) a recepção de um byte vindo do transceiver RF (subcamada PHY). Se, após a recepção desse byte, um quadro completo e livre de erros foi recebido, (2) ele é repassado à subcamada ARQ. Se for um quadro de dados, uma confirmação é gerada e transmitida via subcamada de enquadramento, conforme passos 3 e 4, e (5) o conteúdo do quadro é entregue à aplicação. Se for um quadro de confirmação, os passos 3 a 5 não são executados.
• Timeout e retransmissão: na ocorrência de um (1) timeout na subcamada ARQ, o último quadro de dados é retransmitido, conforme passos 2 e 3.

Do ponto de vista do modelo de sistema, uma questão importante trata da identificação e tratamento dos eventos pelo protocolo. Conforme as sequências exemplificadas, há estes eventos:

• mensagem vinda da aplicação
• bytes vindos da camada física
• timeout

Assim, devem-se investigar técnicas para possibilitar que o protocolo consiga atender esses eventos assim que surgirem.

Multiplexação do acesso a descritores de arquivos

Pelo diagrama sobre a integração ao subsistema de rede do Linux (mostrado na próxima seção), o driver do protocolo de enlace deve ler dados tanto do descritor de arquivo da interface tun quanto da interface serial do transceiver RF. Porém, ao tentar ler algo de um descritor de arquivos (ex: com chamada de sistema read) o processo é bloqueado. Enquanto estiver bloqueado não se pode ler dados que porventura estejam disponíveis no outro descritor de arquivos. Isso se deve ao fato de que leituras com read serem bloqueantes. Para poder aguardar por dados em ambos descritores de arquivo simultaneamente, o processo do protocolo deve multiplexar o acesso a esses descritores.

Algumas técnicas são bem conhecidas para aguardar dados através de múltiplos descritores de arquivos:

1. Espera ocupada: os descritores de arquivo são configurados para serem não-bloqueantes, e assim pode-se implementar um laço que tente ler algo de cada descritor de arquivo em sequência. Se um descritor não tiver dados disponíveis, a leitura retorna imediatamente. Esse tipo de solução tem a grande desvantagem de desperdiçar tempo de processador.
2. Uso de threads: cria-se uma thread para ler de cada descritor de arquivo. Como threads são concorrentes, uma thread pode ficar bloqueada esperando dados em um descritor de arquivo enquanto outra lê outro descritor e processa os dados recebidos. Uma solução como essa envolve um projeto cuidadoso para tratar questões de sincronismo das threads.
3. Uso da chamada de sistema select: a chamada select possibilita esperar por dados em um conjunto de descritores de arquivos. A chamada em si é bloqueante, porém retorna imediatamente se ao menos um dos descritores de arquivos estiver disponível para acesso. A chamada informa quais descritores podem ser acessados sem risco de bloqueio. Essa solução é simples e não precisa dos cuidados com sincronismo como no caso de threads. O exemplo a seguir mostra o uso de select para esperar por dados vindos da entrada padrão ou a recepção de uma conexão em um socket TCP.

Exemplo mais simples de uso de select

Em C++ #include <sys/select.h> #include <sys/time.h> #include <unistd.h> #include <iostream> #include <fcntl.h> using namespace std; int main() { int fd1, fd2; // fd1: arquivo /dev/random (lento de ler) // note que foi aberto em modo não-bloqueante fd1 = open("/dev/random", O_RDONLY | O_NONBLOCK); // fd2: entrada padrão (usualmente teclado) fd2 = 0; // faz com que fd2 opere em modo não-bloqueante int op = fcntl(fd2, F_GETFL); fcntl(fd2, F_SETFL, op | O_NONBLOCK); while (true) { // cria um conjunto de descritores fd_set r; // inicia o conjunto de descritores, e nele // acrescenta fd1 e fd2 FD_ZERO(&r); FD_SET(fd1, &r); FD_SET(fd2, &r); // chama select para monitorar o conjunto de descritores // como não foi especificado timeout (último // parâmetro), select pode ficar bloqueado para sempre // O valor de retorno de seelct é a quantidade de // descritores prontos para serem acessados int n = select(fd1+1, &r, NULL, NULL, NULL); cout << "Ha " << n << " descritores prontos" << endl; // testa se fd1 está pronto para ser acessado if (FD_ISSET(fd1, &r)) { char buffer[1024]; cout << "Descritor do random: "; cout << read(fd1, buffer, 1024) << " bytes" << endl; } // testa se fd1 está pronto para ser acessado if (FD_ISSET(fd2, &r)) { char buffer[1024]; cout << "Descritor do teclado: "; cout << read(fd2, buffer, 1024) << " bytes" << endl; } } } Em Python #!/usr/bin/python3 import sys,select,os import fcntl def set_nonblock(arq): fd = arq.fileno() flag = fcntl.fcntl(fd, fcntl.F_GETFL) fcntl.fcntl(fd, fcntl.F_SETFL, flag | os.O_NONBLOCK) fd1 = open('/dev/random','rb') fd2 = sys.stdin set_nonblock(fd1) set_nonblock(fd2) while True: r,w,e = select.select([fd1, fd2], [], []) if fd1 in r: print('Chegou algo em random:', len(fd1.read(1024))) if fd2 in r: print('Chegou algo no teclado:', len(fd2.read(1024)))

Exemplo de uso de select com socket

Em C #include <sys/select.h> #include <sys/time.h> #include <sys/types.h> #include <sys/socket.h> #include <netinet/in.h> #include <arpa/inet.h> #include <unistd.h> #include <stdio.h> #include <string.h> #define PORT 5555 int cria_socket(int port) { int sd = socket(AF_INET, SOCK_STREAM, 6); struct sockaddr_in addr; socklen_t len; // Vincula um endereco local qualquer ao socket addr.sin_family = AF_INET; addr.sin_addr.s_addr = htonl(INADDR_ANY); addr.sin_port = htons(port); len = sizeof(addr); int ok = 1; setsockopt(sd, SOL_SOCKET, SO_REUSEADDR, (void*)&ok, sizeof(ok)); if (bind(sd, (struct sockaddr*)&addr, sizeof(addr)) < 0) { perror("Ao vincular endereço ao socket"); return -1; } listen(sd, 2); return sd; } int main() { printf("Esperando que se tecle algo + ENTER, ou se receba conexão no port %d ...\n\n", PORT); fflush(stdout); int fd = 0; // o descritor 0 corresponde à entrada padrão ... int sd = cria_socket(PORT); // cria um socket TCP no port PORT int max_fd = fd; if (sd > max_fd) max_fd = sd; struct timeval timeout; // para especificar o timeout timeout.tv_sec = 5; //timeout de 2 segundos timeout.tv_usec = 0; fd_set espera; // um conjunto de descritores FD_ZERO(&espera); // zera o conjunto de descritores FD_SET(fd, &espera); // adiciona "fd" ao conjunto de descritores FD_SET(sd, &espera); // adiciona "sd" ao conjunto de descritores // aqui se usa select para monitorar os descritores contidos em "espera" if (select(max_fd+1, &espera, NULL, NULL, &timeout) == 0) { // timeout !! puts("Timeout !"); } else { puts("Algo chegou ..."); // a seguir se verifica que descritores podem ser lidos sem risco de bloqueio // i.e.: que descritores estão prontos para serem acessados if (FD_ISSET(fd, &espera)) { char linha[128]; int n; n = read(fd, linha, 128); printf("Leu %d caracteres da entrada padrão: %s\n", n, linha); } if (FD_ISSET(sd, &espera)) { char * msg = "***\r\nrecebi conexão mas desconectei em seguida ...\r\n\r\n"; int n, con; struct sockaddr_in addr; socklen_t len = sizeof(addr); con = accept(sd, (struct sockaddr*)&addr, &len); printf("Recebeu conexão de (%s,%d)\n", inet_ntoa(addr.sin_addr), ntohs(addr.sin_port)); send(con, msg, strlen(msg), 0); shutdown(con, SHUT_RDWR); } } } Em Python #!/usr/bin/python3 import sys,socket import select import os,fcntl PORT = 5555 Timeout = 30 def set_nonblock(arq): fd = arq.fileno() flag = fcntl.fcntl(fd, fcntl.F_GETFL) fcntl.fcntl(fd, fcntl.F_SETFL, flag | os.O_NONBLOCK) def cria_socket(port): sd = socket.socket(socket.AF_INET, socket.SOCK_STREAM) sd.setsockopt(socket.SOL_SOCKET, socket.SO_REUSEADDR, 1) sd.bind(('0.0.0.0', port)) sd.listen(2) return sd print("Esperando que se tecle algo + ENTER, ou se receba conexão no port %d ...\n" % PORT) fd1 = sys.stdin set_nonblock(fd1) sd = cria_socket(PORT) while True: r, w, e = select.select([fd1, sd], [], [], Timeout) if not r: print('Timeout ! saindo ...') break if fd1 in r: data = fd1.read(1024) print('Leu %d caracteres da entrada padrão: %s' % (len(data), data)) if sd in r: con,addr = sd.accept() con.send('***\r\nrecebi conexão mas desconectei em seguida ...\r\n\r\n'.encode('utf-8')) con.shutdown(socket.SHUT_RDWR) print('Recebeu conexão de %s:%d' % addr)

Excetuando a técnica 1, as demais podem ser usadas na implementação do protocolo.

A integração com o subsistema de rede do Linux

A integração do protocolo de enlace com o subsistema de rede do Linux pode ser feita de duas formas:

1. Criação de um device driver no kernel Linux: uma tarefa árdua, e que envolve um bom conhecimento sobre o kernel Linux e desenvolvimento de device drivers. A depuração é difícil. O protocolo fica bem integrado ao sistema operacional.
2. Implementação do protocolo em espaço de usuário: um protótipo em espaço de usuário é mais fácil de criar, pois pode usar as APIs existentes para a linguagem de programação escolhida. A depuração fica facilitada. Porém a integração com o sistema operacional apresenta um certo overhead devido ao fluxo de processamento transitar frequentemente entre espaços de sistema e de usuário.

Para o objetivo do projeto 1, a segunda opção é a mais adequada. A implementação em espaço de usuário deve usar uma interface de rede do tipo tun para fazer a integração com o subsistema de rede. Com isso, existe uma interface de rede associada ao enlace estabelecido pelo protocolo, a qual possui parâmetros de rede IP (endereço, máscara), e rotas podem ser definidas para destinos alcançáveis através dela. Com isso, qualquer aplicação TCP/IP pode se comunicar usando o protocolo desenvolvido.

A figura a seguir mostra um diagrama que esquematiza a integração do protótipo com o Linux, evidenciando a interface de rede do tipo tun.

A criação e configuração de uma interface tun pode ser feita de forma programática, usando chamadas de sistema do Linux. O código-fonte a seguir demonstra como uma interface dessas pode ser criada e configurada.

função para criar uma interface tun

#include <sys/types.h> #include <unistd.h> #include <fcntl.h> #include <sys/ioctl.h> #include <stdio.h> #include <net/if.h> #include <linux/if_tun.h> #include <string.h> #include <sys/socket.h> #include <netinet/in.h> #include <arpa/inet.h> // tun_alloc: cria uma interface tun // Parâmetro de entrada: // char * dev: o nome da interface ser criada. Se for NULL, interface será denominada pelo sistema (ex: tun0) // // Retorno: valor inteiro // - se > 0: o descritor de arquivo da interface tun criada. // - se < 0, ocorreu um erro #define MTU 256 #define MASK "255.255.255.252" int tun_alloc(char *dev) { struct ifreq ifr; int fd, err; if( (fd = open("/dev/net/tun", O_RDWR)) < 0 ) { perror(""); return -1; } memset(&ifr, 0, sizeof(ifr)); /* Flags: IFF_TUN - TUN device (no Ethernet headers) * IFF_TAP - TAP device * * IFF_NO_PI - Do not provide packet information */ //ifr.ifr_flags = IFF_TUN | IFF_NO_PI; ifr.ifr_flags = IFF_TUN; if( *dev ) strncpy(ifr.ifr_name, dev, IFNAMSIZ); err = ioctl(fd, TUNSETIFF, (void *) &ifr); if( err < 0 ){ close(fd); perror(""); return err; } return fd; } // esta outra função configura a interface tun: define os endereços IP do enlace ponto-a-ponto, // a máscara de rede /30 e ativa a interface. Ela faz o mesmo que o comando: // ifconfig nome_tun IP_da_interface dstaddr IP_da_outra_ponta_do_enlace // // esta função deve ser usada assim, supondo que a interface tun se chame tun0, e os endereços IP // do enlace sejam 10.0.0.1 e 10.0.0.2: // // if (set_ip("tun0", "10.0.0.1", "10.0.0.2") < 0) { // perror("so configurar a interface tun"); // return 0; // } // // Maiores detalhes sobre as chamadas de sistemas utilizadas: ver "man netdevice", ou // http://man7.org/linux/man-pages/man7/netdevice.7.html int set_ip(char *dev, char * ip, char * dst) { struct ifreq ifr; struct sockaddr_in *addr; int ok; int sd; // cria um socket para configurar a interface // esse socket não tem nada de especial ... sd = socket(AF_INET, SOCK_DGRAM, 0); if (sd < 0) return sd; // zera todos os bytes da struct ifreq // essa struct contém os atributos a serem configurados na interface bzero(&ifr, sizeof(ifr)); // usa o ponteiro addr para referenciar o campo de endereço da struct ifreq // isso facilita o preenchimento dos atributos desse campo addr = (struct sockaddr_in*)&(ifr.ifr_ifru.ifru_addr); // preenche o campo endereço com o enderço IP da interface addr->sin_addr.s_addr = inet_addr(ip); addr->sin_family = AF_INET; addr->sin_port = 0; // escreve o nome da interface na struct ifreq. Isso é necessário // para o kernel saber que interface é alvo da operação strncpy(ifr.ifr_name, dev, IFNAMSIZ); // executa uma operação de configuração de endereço IP de interface ok = ioctl(sd, SIOCSIFADDR, &ifr); if (ok < 0) return ok; // preenche o campo endereço com o endereço IP da outra ponta do enlace addr->sin_addr.s_addr = inet_addr(dst); // executa uma operação de configuração de endereço IP de destino da interface ok = ioctl(sd, SIOCSIFDSTADDR, &ifr); if (ok < 0) return ok; // preenche o campo endereço com a máscara de rede da interface addr->sin_addr.s_addr = inet_addr(MASK); // executa uma operação de configuração de máscara de rede da interface ok = ioctl(sd, SIOCSIFNETMASK, &ifr); if (ok < 0) return ok; // executa uma operação de configuração de MTU da interface ifr.ifr_mtu = MTU; ok = ioctl(sd, SIOCSIFMTU, &ifr); if (ok < 0) return ok; // lê as flags da interface ok = ioctl(sd, SIOCGIFFLAGS, &ifr); if (ok < 0) return ok; // acrescenta flags UP (ativa) e RUNNING (pronta para uso) ifr.ifr_flags |= IFF_UP | IFF_RUNNING; // executa uma operação de configuração flags da interface return ioctl(sd, SIOCSIFFLAGS, &ifr); }

Após criar a interface, pode-se testar a comunicação com um simples ping:

ping 10.0.0.2

Atividade

1. Integre seu protocolo com o kernel Linux. Antes de qualquer coisa, o enquadramento e a detecção de erros devem estar funcionando corretamente.
2. Escolha a técnica de multiplexação a ser usada. Dica: dedique um tempo a modelar seu protocolo, para evidenciar como seus elementos atuarão de acordo com a multiplexação escolhida ... e lembre de considerar a implementação de timeouts.

05/04: Projeto 1: o tratamento de eventos por meio do dispatcher

A estrutura do protocolo envolve o uso de um dispatcher (ou um event loop) para identificar os eventos e encaminhá-los para serem tratados pelos componentes do protocolo. Quando o dispatcher identifica um evento, ele invoca de forma síncrona seu tratador. As sequências de processamento do protocolo descritas na aula de 22/03 correspondem às chamadas dos tratadores de evento. Na aba colapsada a seguir apresenta-se um esboço de um dispatcher, que pode ser adaptado para uso no protocolo.

um esboço do Dispatcher

Diagrama de classes UML para o esboço do Dispatcher. DemoHandler1 e DemoHandler são apenas ilustrativos, para exemplificar handlers definidos por especialização da classe Handler #ifndef DISPATCHER_H #define DISPATCHER_H #include <unistd.h> #include <fcntl.h> #include <vector> using std::vector; class Handler { protected: int fd; // descritor a ser monitorado Handler * upper, * lower; bool enabled; // indica se este Handler deve ser monitorado pelo Dispatcher timeval to_end; // tempo de referência para o timeout public: Handler(int descriptor); ~Handler() {} virtual void handle_data() = 0; virtual void handle_timeout() = 0; int get_descriptor() const { return fd;} virtual int receive(char * buffer, int len) = 0; virtual int send(char * buffer, int len) = 0; virtual void set_upper(Handler & h) { upper = &h;} virtual void set_lower(Handler & h) { lower = &h;} void enable() { enabled = true;} void disable() { enabled = false;} bool active() const { return enabled;} // retorna valor de timeout em milissegundos // se retornar 0 (zero), então não há timeout a ser verificado int get_timeout() const; bool timeout_exceeded() const; protected: // para iniciar um timeout (para uso interno) void start_timeout(int t_out); // para cancelar timeout void stop_timeout(); }; class Dispatcher { private: vector<Handler*> handlers; public: Dispatcher() {} ~Dispatcher() {} void add_handler(Handler & h); void loop(); }; #endif dispatcher.h #include <sys/select.h> #include <sys/time.h> #include "dispatcher.h" /***************************************** * classe Handler *****************************************/ Handler::Handler(int descriptor) : fd(descriptor), upper(nullptr), lower(nullptr) { int op = fcntl(fd, F_GETFL); fcntl(fd, F_SETFL, op | O_NONBLOCK); enabled = true; } int Handler::get_timeout() const { timeval agora; // sem timeout por enquanto ... if (to_end.tv_sec == 0 and to_end.tv_usec == 0) return 0; gettimeofday(&agora, NULL); int t_out = (to_end.tv_sec - agora.tv_sec) * 1000; t_out += (to_end.tv_usec - agora.tv_usec) / 1000; return t_out; } bool Handler::timeout_exceeded() const { return get_timeout() < 0; } void Handler::start_timeout(int t_out) { gettimeofday(&to_end, NULL); long us = to_end.tv_usec + t_out * 1000; to_end.tv_sec += us / 1000000; to_end.tv_usec = us % 1000000; } void Handler::stop_timeout() { to_end.tv_sec = 0; to_end.tv_usec = 0; } /***************************************** * classe Dispatcher *****************************************/ void Dispatcher::add_handler(Handler & h) { handlers.push_back(&h); } void Dispatcher::loop() { while (true) { // cria um conjunto de descritores fd_set r; int fd_max = 0; // descritor com maior valor // inicia o conjunto de descritores, e nele // acrescenta descritores dos handlers // também determina o menor valor de timeout FD_ZERO(&r); int tmin = -1; for (auto h : handlers) { if (h->active()) { int fd = h->get_descriptor(); if (fd > fd_max) fd_max = fd; FD_SET(fd, &r); } int tout = h->get_timeout(); if (tout > 0) { if (tmin < 0) tmin = tout; else if (tmin > tout) tmin = tout; } } // define o valor de timeout a ser usado pelo select // se nenhum handler definiu um timeout, então select também // não tem timeout timeval timeout; timeval * to_ptr = NULL; if (tmin > 0) { timeout.tv_sec = tmin / 1000; timeout.tv_usec = 1000 * (tmin % 1000); to_ptr = &timeout; } // chama select para monitorar o conjunto de descritores // O valor de retorno de select é a quantidade de // descritores prontos para serem acessados int n = select(fd_max+1, &r, NULL, NULL, to_ptr); if (n == 0) { // timeout ... for (auto h : handlers) { if (h->timeout_exceeded()) h->handle_timeout(); } } else { for (auto h : handlers) { if (h->active()) { int fd = h->get_descriptor(); // testa se descritor está pronto para ser acessado if (FD_ISSET(fd, &r)) h->handle_data(); } } } } } dispatcher.cpp #include <iostream> #include <stdio.h> #include "dispatcher.h" using namespace std; void dump(char * buffer, int len) { int m = 0, line = 0; while (m < len) { printf("%02X: ", line*16); for (int n=0; n < 16 and m < len; n++, m++) { int x = (unsigned char)buffer[m]; printf("%02X ", x); } puts(""); line++; } } // define um handler de demonstração class DemoHandler1 : public Handler { public: DemoHandler1(int desc) : Handler(desc) {} ~DemoHandler1() {} virtual void handle_data() { char buffer[1024]; int n = read(fd, buffer, 1024); cout << "Recebeu " << n << " bytes vindos do descritor " << fd << ": "; dump(buffer, n); cout << endl; } virtual void handle_timeout() {} // não implementado virtual int send(char * buffer, int len) {} // não implementado virtual int receive(char * buffer, int len) {} // não implementado }; int main() { DemoHandler1 h1(0); // handler vinculado à entrada padrão DemoHandler1 h2(open("/dev/random", O_RDONLY | O_NONBLOCK)); // handler vinculado ao PRNG Dispatcher monitor; monitor.add_handler(h1); monitor.add_handler(h2); monitor.loop(); } main.cpp: programa de demonstração do dispatcher

a classe Enquadramento redefinida como um Handler

class Enquadramento : public Handler { public: Enquadramento(Serial & dev, int bytes_min, int bytes_max); virtual ~Enquadramento(); // envia o quadro apontado por buffer // o tamanho do quadro é dado por bytes virtual int send(char * buffer, int bytes); virtual int receive(char * buffer, int bytes) { throw -1;} virtual void handle_data(); virtual void handle_timeout(); private: int min_bytes, max_bytes; // tamanhos mínimo e máximo de quadro Serial & porta; char buffer[4096]; enum Estados {Q0, Q1, Q2}; // bytes recebidos pela MEF até o momento int n_bytes; // estado atual da MEF int estado; // aqui se implementa a máquina de estados de recepção // retorna true se reconheceu um quadro completo bool handle(char byte); // verifica o CRC do conteúdo contido em "buffer". Os dois últimos // bytes desse buffer contém o valor de CRC bool check_crc(char * buffer, int len); // gera o valor de CRC dos bytes contidos em buffer. O valor de CRC // é escrito em buffer[len] e buffer[len+1] void gen_crc(char * buffer, int len); // calcula o valor de CRC dos bytes contidos em "cp". // "fcs" deve ter o valor PPPINITFCS16 // O resultado é o valor de CRC (16 bits) // OBS: adaptado da RFC 1662 (enquadramento no PPP) u16 pppfcs16(char * cp, int len); }; Enquadramento.h: note que método envia foi substituído por send, sumiu método recebe, e foram adicionados handle_data e handle_timeout Enquadramento::Enquadramento(Serial & dev, int bytes_min, int bytes_max) : Handler(dev.get()), porta(dev) { min_bytes = bytes_min; max_bytes = bytes_max; n_bytes = 0; estado = Q0; } int Enquadramento::send(char * buffer, int bytes) { // envio de um quadro } void Enquadramento::handle_data() { char byte; porta.read(&byte, 1); if (handle(byte)) { // recebeu um quadro completo: repassa-o para ARQ if (upper) upper->receive(buffer, n_bytes); } } Enquadramento.cpp (apenas os métodos novos ou modificados)

a criação do protocolo supondo que existam as classes ARQ e Enquadramento

#include "dispatcher.h" #include "Enquadramento.h" #include "ARQ.h" #include "Serial.h" #include "Tun.h" int main() { Serial dev("/dev/ttyUSB0", B9600); int tun_fd = tun_alloc("ptp0"); ARQ h1(tun_fd); // handler ARQ Enquadramento h2(dev, 32, 256); // handler Enquadramento // ARQ em cima, Enquadramento embaixo h1.set_lower(h2); h2.set_upper(h1); Dispatcher monitor; monitor.add_handler(h1); monitor.add_handler(h2); monitor.loop(); } main.cpp

10/04: Projeto 1: O controle de acesso ao meio

O enlace a ser estabelecido usa um canal compartilhado. Somente um dos lados do enlace pode transmitir em um determinado momento. Por isso é necessário que o protocolo inclua um mecanismo de controle de acesso ao meio (MAC) para arbitrar as transmissões no enlace.

Três abordagens para acesso ao meio podem ser identificadas (maiores detalhes estão no capítulo 5, seção 5.3, do livro Redes de Computadores e a Internet, 5a. edição, de James Kurose e Keith Ross):

1. Por revezamento: usando mensagens especiais, o direito de acesso ao meio é definido inequivocamente para cada um dos lados alternadamente. Esse acesso ao meio é livre de disputa, o que significa que colisões não ocorrem.
2. Por divisão de tempo: ambos os lados se mantêm sincronizados, e usam intervalos de tempo cíclicos predeterminados para suas transmissões (isso é uma forma de TDMA). Essa abordagem também é livre de disputa.
3. Aleatória: cada um dos lados pode tentar transmitir em instantes arbitrários. Se transmissões se sobrepuserem (colisões), as mensagens envolvidas são perdidas e devem ser retransmitidas. Usam-se esperas de tempo aleatórias para evitar que as retransmissões causem novas colisões. Essa abordagem envolve disputa por acesso ao meio.

Para nosso protocolo, as abordagens 1 e 3 são viáveis. Para a abordagem 1, pode-se imaginar um acesso ao meio do tipo mestre-escravo. Para a abordagem 3, o acesso ao meio clássico Aloha poderia ser facilmente implementado.

Aloha

Um controle de acesso ao meio do tipo Aloha. Ele pode ser integrado ao ARQ:

Mestre-escravo

Um controle de acesso ao meio do tipo Mestre-Escravo. Ele também pode ser integrado ao ARQ:

Atividade

1. Escolha um dos MAC e incorpore-o a seu protocolo.

Diferenciação de eventos no ARQ

O componente ARQ está sujeito a pelo menos três tipos de eventos:

• payload vindo da tun: notificado pelo Dispatcher por meio do método handle_data
• quadro vindo do Enquadramento: notificado pelo Enquadramento por meio do método receive
• timeout: notificado pelo Dispatcher por meio do método handle_timeout.

Esses eventos devem ser tratados por meio da máquina de estados do ARQ. Uma forma de resolver isso é implementar a máquina de estados em um método específico, como este:

// executa a MEF, passando como parâmetros uma identificação
// do tipo de evento, o buffer que contém os dados, 
// e a quantidade de bytes contidos nesse buffer
void mef(Evento tipo, char * dados, int bytes);

Método mef, que representa a máquina de estados. Ele deve ser declarado na classe ARQ

O tipo Evento pode ser declarado como uma enumeração:

enum Evento {Payload, Quadro, Timeout};

Tipo Evento: fica melhor declará-lo como privativo da classe ARQ

Seguindo esse modelo, os eventos recebidos podem ser encaminhados para a máquina de estados pelos respectivos métodos da classe ARQ:

void ARQ::receive(char * frame, int bytes) {
  mef(Quadro, frame, bytes);
}

void ARQ::handle_data() {
  char buffer[1024];
  int bytes;

  // lê os bytes da tun
  
  // encaminha os dados lidos para a máquina de estados
  mef(Payload, buffer, bytes);
}

void ARQ::handle_timeout() {
  // encaminha o timeout pra máquina de estados
  mef(Timeout, NULL, 0);
}

Métodos que recebem eventos devem encaminhá-los apropriadamente para a máquina de estados

12/04: Projeto 1: Timeouts

O protocolo de enlace possui limites de tempo para suas sequências de ações em ao menos estes casos:

• Enquadramento: há um limite de tempo para a recepção de um novo byte de um quadro. Se esse tempo for excedido, considera-se que os bytes restantes foram perdidos e assim o quadro incompleto deve ser descartado.
• ARQ: há um limite de tempo para a recepção de uma confirmação de um quadro de dados. Se esse tempo for excedido, uma retransmissão deve ser feita.
• MAC:
  • Aloha: o MAC Aloha realiza backoff quando um quadro é perdido. O backoff pode ser considerado um tempo de espera a ser notificado ao MAC, de forma parecida com um timeout.
  • Mestre-escravo: no MAC Mestre-Escravo cada nodo pode deter o direito de transmitir por um tempo máximo predefinido. Quando esse temnpo se esgota o nodo deve passar o direito de transmissão para o outro nodo. O controle do tempo de posse do direito de transmitir pode ser implementado de forma parecida com timeout.

No modelo de implementação do protocolo, cabe ao Dispatcher detectar e notificar timeouts. Porém o Dispatcher não sabe qual timeout pertence a cada Handler, ou que timeouts os Handlers precisam. Assim, os Handlers precisam disposnibilizar essa informação ao Dispatcher.

Dispatcher e Handler com suporte a timeout

O Handler com suporte a timeout #ifndef DISPATCHER_H #define DISPATCHER_H #include <unistd.h> #include <fcntl.h> #include <vector> using std::vector; class Handler { protected: int fd; // descritor a ser monitorado Handler * upper, * lower; bool enabled; // indica se este Handler deve ser monitorado pelo Dispatcher timeval to_end; // tempo de referência para o timeout public: Handler(int descriptor); ~Handler() {} virtual void handle_data() = 0; virtual void handle_timeout() = 0; int get_descriptor() const { return fd;} virtual int receive(char * buffer, int len) = 0; virtual int send(char * buffer, int len) = 0; virtual void set_upper(Handler & h) { upper = &h;} virtual void set_lower(Handler & h) { lower = &h;} void enable() { enabled = true;} void disable() { enabled = false;} bool active() const { return enabled;} // retorna valor de timeout em milissegundos // se retornar 0 (zero), então não há timeout a ser verificado int get_timeout() const; bool timeout_exceeded() const; protected: // para iniciar um timeout (para uso interno) void start_timeout(int t_out); // para cancelar timeout void stop_timeout(); }; class Dispatcher { private: vector<Handler*> handlers; public: Dispatcher() {} ~Dispatcher() {} void add_handler(Handler & h); void loop(); }; #endif dispatcher.h #include <sys/select.h> #include <sys/time.h> #include "dispatcher.h" /***************************************** * classe Handler *****************************************/ Handler::Handler(int descriptor) : fd(descriptor), upper(nullptr), lower(nullptr) { int op = fcntl(fd, F_GETFL); fcntl(fd, F_SETFL, op | O_NONBLOCK); enabled = true; } int Handler::get_timeout() const { timeval agora; // sem timeout por enquanto ... if (to_end.tv_sec == 0 and to_end.tv_usec == 0) return 0; gettimeofday(&agora, NULL); int t_out = (to_end.tv_sec - agora.tv_sec) * 1000; t_out += (to_end.tv_usec - agora.tv_usec) / 1000; return t_out; } bool Handler::timeout_exceeded() const { return get_timeout() < 0; } void Handler::start_timeout(int t_out) { gettimeofday(&to_end, NULL); long us = to_end.tv_usec + t_out * 1000; to_end.tv_sec += us / 1000000; to_end.tv_usec = us % 1000000; } void Handler::stop_timeout() { to_end.tv_sec = 0; to_end.tv_usec = 0; } /***************************************** * classe Dispatcher *****************************************/ void Dispatcher::add_handler(Handler & h) { handlers.push_back(&h); } void Dispatcher::loop() { while (true) { // cria um conjunto de descritores fd_set r; int fd_max = 0; // descritor com maior valor // inicia o conjunto de descritores, e nele // acrescenta descritores dos handlers // também determina o menor valor de timeout FD_ZERO(&r); int tmin = -1; for (auto h : handlers) { if (h->active()) { int fd = h->get_descriptor(); if (fd > fd_max) fd_max = fd; FD_SET(fd, &r); } int tout = h->get_timeout(); if (tout > 0) { if (tmin < 0) tmin = tout; else if (tmin > tout) tmin = tout; } } // define o valor de timeout a ser usado pelo select // se nenhum handler definiu um timeout, então select também // não tem timeout timeval timeout; timeval * to_ptr = NULL; if (tmin > 0) { timeout.tv_sec = tmin / 1000; timeout.tv_usec = 1000 * (tmin % 1000); to_ptr = &timeout; } // chama select para monitorar o conjunto de descritores // O valor de retorno de select é a quantidade de // descritores prontos para serem acessados int n = select(fd_max+1, &r, NULL, NULL, to_ptr); if (n == 0) { // timeout ... for (auto h : handlers) { if (h->timeout_exceeded()) h->handle_timeout(); } } else { for (auto h : handlers) { if (h->active()) { int fd = h->get_descriptor(); // testa se descritor está pronto para ser acessado if (FD_ISSET(fd, &r)) h->handle_data(); } } } } } dispatcher.cpp

19/04: Gerenciamento de sessão

A próxima função do protocolo de enlace envolve o estabelecimento, manutenção e terminação de conexão. Sendo um protocolo ponto-a-ponto, deve-se estabelecer um enlace entre as duas pontas participantes antes de poder transferir dados. Isso evita que as transmissões entre um par de participantes sejam confundidas com transmissões de outros pares.

Nas seções 5.2 e 5.3 do capítulo 5 do livro Protocol Engineering, 2nd ed, de Hartmut Konig, há uma explicação sobre o gerenciamento de conexões e diversas formas de implementá-la. No caso do protocolo de enlace, serão usados estabelecimento e terminação explícitos de conexões, e manutenção de conexão.

Estabelecimento de conexão

Para criar uma conexão deve-se:

• estabelecer a conexão: ambos participantes devem se sincronizar para aceitar ou recusar a conexão
• negociar parâmetros de conexão: a conexão pode envolver parâmetros operacionais do protocolo que devem ser comuns a ambos participantes. Como exemplo, citam-se tamanho máximo de PDU e identificador de conexão.

A sincronização entre os participantes implica a troca de mensagens, a qual pode ser feita com duas (2-way handshaking) ou 3 (3-way handshaking) mensagens:

A sincronização do tipo 2-way é adequada em comunicações unidirecionais, mas não para comunicações bidirecionais. Isso se deve ao fato de que a primeira mensagem (CR) contém parâmetros de conexão do participante que iniciou o processo, e a segunda mensagem (CC) contém parâmetros do outro participante. Se a mensagem CC for perdida, o participante iniciador da conexão não tem como saber se a conexão foi aceita e quais os parâmetros definidos pelo outro participante. Assim, uma terceira mensagem enviada pelo iniciador serve para que o outro participante saiba que a conexão foi estabelecida, e que assim ele pode usá-la para enviar dados. De forma resumida:

1. Ao receber a mensagem CC, o iniciador já pode enviar dados pela conexão
2. Ao receber a terceira mensagem, o outro participante também pode enviar dados pela conexão. OBS: essa terceira mensagem pode ser uma mensagem de dados comum, pois ela serve para que o outro participante saiba que a conexão foi estabelecida com os parâmetros negociados.

Manutenção de conexão

Um enlace pode ter momentos de ociosidade, quando não há mensagens de dados para serem transmitidas. Isso pode ser confundido com casos em que o enlace se rompe (ex: um dos participantes é desligado, ou o meio de comunicação é seccionado). Para evitar que um enlace rompido seja interpretado com um enlace ocioso (e vice-versa), o protocolo deve fazer a manutenção de conexão.

A manutenção de conexão pode ser feita com o envio periódico de mensagens de verificação. Por exemplo, o protocolo PPP usa mensagens Keep-Alive enviadas a cada 10 segundos para monitorar o estado do enlace. Se três mensagens Keep-Alive consecutivas forem perdidas, o enlace é terminado. Nesse caso, após um certo tempo (ex: 30 segundos) o protocolo PPP tenta restabelecer o enlace. O protocolo TCP também possui um mecanismo opcional para manutenção de conexão chamado de Keep Alive. Uma abordagem como essa poderia ser incluída no protocolo de enlace em desenvolvimento.

Terminação de conexão

A terminação de conexão implica duas necessidades:

1. A sincronização entre os participantes quanto ao término da conexão (ambos participantes devem fechar a conexão)
2. A garantia de que todas as mensagens de dados pendentes sejam entregues

A solução não é tão simples quanto parece. Uma discussão detalhada pode ser lida na seção 5.3.3 do livro Protocol Engineering, 2nd ed, de Hartmut Konig. Com base nessa explicação e no fato de que o protocolo de enlace em desenvolvimento é bidirecional, deve-se usar a terminação de conexão feita por ambos participantes do enlace. Assim um participante envia uma mensagem para terminação de conexão, e após sua confirmação entra-se em estado de conexão parcialmente fechada (half-close connection). O outro participante envia suas mensagens pendentes, e em seguida envia sua mensagem de terminação de conexão. Após a confirmação dessa última mensagem de terminação, a conexão é considerada terminada. A figura a seguir exemplifica esse procedimento.

Uma simplificação pode ser feita se ambos participantes encerrarem a conexão simultaneamente. Nesse caso, a terminação pode ser sincronizada com três mensagens (3-way handshake):

Por fim, pode acontecer de mensagens de terminação de conexão serem perdidas. Isso manteria um ou mesmo ambos participantes esperando indefinidamente pelo término de conexão. Uma solução para evitar essa situação é usar timeout para a espera de confirmação da mensagem de término de conexão.

Atividade

1. Identifique em que parte da estrutura do seu protocolo devem se encaixar o gerenciamento de conexão
2. Modele o gerenciamento de conexão do seu protocolo de enlace.

24/04: Projeto 1: conclusão

O protocolo ponto-a-ponto para um canal sem-fio entra em fase de conclusão. O modelo do protocolo foi estabelecido de forma a prover os serviços que foram definidos no início do projeto. Apenas o controle de conexão é opcional.

Para as equipes que puderem implementar o controle de conexão, segue um esboço de como isso se integraria na estrutura atual do protocolo.

O protocolo com o controle de conexão

O controle de conexão implica estabelecimento, manutenção e terminação de conexões. Apenas uma conexão pode estar estabelecida por vez, pois no contexto do protocolo uma conexão significa uma associação com outra entidade do protocolo para formar um enlace ponto-a-ponto. Com isso, apenas um enlace ponto-a-ponto pode existir por vez, para uma determinada entidade de protocolo. O estabelecimento de conexão envolve uma negociação em três vias, e a terminação deve ser feita explicitamente por ambas entidades. O comportamento do controle de conexão está esboçado na máquina de estados a seguir.

Um possível comportamento para o controle de conexão

Algumas modificações são necessárias para integrar o controle de conexão com a garantia de entrega (ARQ):

• ARQ não mais recebe payload diretamente da tun, e sim via controle de conexão
• Quadro usado no ARQ deve ter em seu cabeçalho um campo para identificar a conexão. Quadros recebidos com identificadores de conexão desconhecidos devem ser descartados pelo ARQ (e sem serem confirmados).
• Quadros de gerenciamento do controle de conexão devem ser enviados sem aguardar confirmação, ou com retransmissões limitadas.
• ARQ deve inibir controle de conexão quando transmitir um quadro de dados, até que receba uma confirmação.

26/04: Projeto 1: finalização

A entrega do código-fonte do protocolo e do relatório técnico deve ser feita usando o Moodle.

• Prazo: 08/05/2017
• Prazo com atraso: 15/05/2017

03/05: Projeto 2: um protocolo de aplicação

Projeto 2: um protocolo de aplicação; especificação e modelagem informal do protocolo

• Objetivo:
  • Propor um protocolo de aplicação
  • Descrever informalmente o protocolo proposto

Visão geral:

• Pedir que a turma proponha uma aplicação que julgue interessante. Algumas ideias são:
  • Transferência de arquivos, com autenticação de usuário, múltiplos arquivos transferidos simultaneamente e procura remota de arquivos.
  • Jogo (obs: sugerir a batalha naval, ou algum jogo simples com múltiplos jogadores)
  • Finanças (ex: compra e venda de ações ... creio que com modelo publisher/subscriber)
  • Sensoriamento e Controle (ex: monitorar janelas, portas e iluminação de uma residência, podendo abri-las ou fechá-las)
  • Comunicador usando rede adhoc com dispositivos móveis

... em seguida:

1. Descrever a comunicação envolvida nessa aplicação
2. Propor um protocolo para essa finalidade
3. Especificar o protocolo (rever os passos 1 a 7 das diretrizes de projeto)
   • Definir o serviço a ser provido pelo protocolo, o que inclui a interface de acesso a serviço
4. Verificar e implementar o protocolo

Exemplo: Protocolo para Jogos

• Writing a Game Server Protocol
• Open Game Protocol
• GSA: Gaming Standards Association

No semestre 2015/2 foi especificado um protocolo genérico para jogos com múltiplos jogadores. Esse protocolo se mostrou complexo para o tempo disponível para desenvolvimento.A seguir apresenta-se sua descrição inicial.

O protocolo para jogos oferece um serviço de comunicação flexível e extensível para jogos com múltiplos jogadores. Esse serviço foi inicialmente imaginado com estas funcionalidades:

1. Identificação e descoberta de jogadores
2. Controle de sessão
   • Entrada/início de jogo
   • Término/abandono de jogo
   • Mudança de modo de jogador (ex: suspensão ou pausa, reativação, ...)
   • Autenticação de jogador
3. Comunicações de jogo
   • Entrega de mensagens diretas (endereçadas a um jogador ou grupo de jogadores), com ou sem resposta
   • Notificações de eventos
   • Envio de mensagens de controle

Especificação do protocolo

• Objetivos:
  • definir o serviço a ser provido pelo protocolo
  • determinar o vocabulário do protocolo
  • especificar suas regras de procedimento usando máquinas de estado finitos

O protocolo de aplicação escolhido deve ser especificado. Isso implica sua descrição sem ambiguidades, para que possa ser corretamente implementado. A especificação envolve a definição do serviço oferecido, seu vocabulário e sintaxe, sua gramática, e a verificação de seu comportamento. Sua implementação se chama entidade de protocolo, sendo composta por software e (por vezes) hardware.

Essas questões já foram vistas no projeto 1:

• Especificação do protocolo no projeto 1

Atividade: modelo do protocolo de aplicação com MEF

1. Defina o vocabulário do protocolo de aplicação, incluindo os tipos de mensagens e suas sintaxes.
2. Modele o comportamento do protocolo de aplicação com uma MEF. Para isso identifique os componentes da MEF capazes de representar as regras de procedimento do protocolo: estados, mensagens e eventos, transições. Em seguida, faça um diagrama da MEF do protocolo.

08/05: Projeto 2: codificação das mensagens

vocabulário e gramática do protocolo; sintaxe: representação textual, ASN.1

Objetivos:

• representar mensagens com sintaxe abstrata (ex: ABNF, ASN.1, ou outras)
• codificar mensagens com sintaxe concreta

Cada mensagem que compõe o vocabulário de um protocolo carrega informações que dizem respeito a seu conteúdo (ou payload) e meta-dados do protocolo. Por exemplo, mensagens do protocolo TCP (chamadas de segmentos), como mostrado na figura a seguir, contêm diversas informações de controle que formam um cabeçalho, e um corpo de mensagem que contém os dados transportados pela mensagem.

O TCP é um protocolo de transporte, e usa uma codificação binária em suas mensagens com representação big endian (todos protocolos da Internet usam essa representação - ver RFC 1700). Já o protocolo de aplicação SMTP (Simple Mail Transfer Protocol) usa uma codificação textual em suas mensagens. O exemplo a seguir mostra a conversação entre um cliente (prefixo C:) e um servidor SMTP (prefixo S:).

S: 220 smtp.example.com ESMTP Postfix

C: HELO relay.example.org 
S: 250 Hello relay.example.org, I am glad to meet you

C: MAIL FROM:<bob@example.org>
S: 250 Ok

C: RCPT TO:<alice@example.com>
S: 250 Ok

C: RCPT TO:<theboss@example.com>
S: 250 Ok

C: DATA
S: 354 End data with <CR><LF>.<CR><LF>

C: From: "Bob Example" <bob@example.org>
C: To: "Alice Example" <alice@example.com>
C: Cc: theboss@example.com
C: Date: Tue, 15 January 2008 16:02:43 -0500
C: Subject: Test message
C: 
C: Hello Alice.
C: This is a test message with 5 header fields and 4 lines in the message body.
C: Your friend,
C: Bob
C: .
S: 250 Ok: queued as 12345

C: QUIT
S: 221 Bye

Outro protocolo de aplicação muito utilizado é o HTTP (Hypertext Transfer Protocol), que usa uma representação híbrida em suas mensagens (predominantemente textual, mas pode ter conteúdo binário).

Requisição (enviada pelo cliente)

Resposta (enviada pelo servidor)

GET /~msobral/ptc/docs/ HTTP/1.1 Host: tele.sj.ifsc.edu.br

HTTP/1.1 200 OK Date: Mon, 21 Sep 2015 17:04:04 GMT Server: Apache Vary: Accept-Encoding Content-Length: 870 Content-Type: text/html;charset=UTF-8 <!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 3.2 Final//EN"> <html> <head> <title>Index of /~msobral/ptc/docs</title> </head> <body> <h1>Index of /~msobral/ptc/docs</h1> <table><tr><th><img src="/icons/blank.gif" alt="[ICO]"></th><th><a href="?C=N;O=D">Name</a> </th><th><a href="?C=M;O=A">Last modified</a></th><th><a href="?C=S;O=A">Size</a></th><th><a href="?C=D;O=A">Description</a></th></tr><tr><th colspan="5"><hr></th></tr> <tr><td valign="top"><img src="/icons/back.gif" alt="[DIR]"></td><td><a href="/~msobral /ptc/">Parent Directory</a></td><td>&nbsp;</td><td align="right"> - </td><td>&nbsp;</td></tr> <tr><td valign="top"><img src="/icons/layout.gif" alt="[ ]"></td><td><a href="state.pdf">state.pdf</a></td><td align="right">08-Sep-2015 16:47 </td><td align="right">130K</td><td>&nbsp;</td></tr> <tr><th colspan="5"><hr></th></tr> </table> </body></html>

Esses exemplos apresentam basicamente dois tipos de codificação:

1. Textual: as informações são representadas em texto legível, o que facilita a interpretação por seres humanos porém gera mensagens mais longas. A representação em texto pode facilitar também o intercâmbio de informações entre computadores com diferentes arquiteturas e aplicações escritas com diferentes linguagens de programação. Por fim, um detalhe importante é a codificação de caractere adotada (ex: no caso do HTTP apresentado, usa-se codificação UTF-8).
2. Binária: as informações são representadas por sequências de bits, segundo algum esquema de codificação, o que gera potencialmente mensagens mais curtas, porém de difícil legibilidade por seres humanos. A representação binária deve seguir regras estritas para o correto intercâmbio entre computadores de diferentes arquiteturas e programas escritos em diferentes linguagens de programação.

Hoje será estudado como cada tipo de representação pode ser especificado.

Sintaxe abstrata

Sintaxe abstrata é a especificação do conjunto de valores que compõem uma estrutura de dados, independente de linguagem de programação e arquitetura de hardware. Por exemplo, para representar um ativo em negociação identificaram-se como informações necessárias o nome do ativo, seu código de negociação, seu valor monetário e a data e horário desse valor. Assim pode-se especificar uma estrutura de dados que represente esse ativo, sendo ela composta de:

NOME: cadeia de caracteres com comprimento máximo de 16 caracteres
CODIGO: numero inteiro
VALOR: numero inteiro (quantidade de centavos)
DATA: string numerica com 8 caracteres (DDMMYYYY)
HORARIO: string numerica com 6 caracteres (HHMMSS)

A descrição acima é a sintaxe abstrata da estrutura de dados. Ela descreve que valores compõem a estrutura, e quais os tipos desses valores. No entanto, ela não especifica sua sintaxe concreta, que determina como essa estrutura de dados é representada, ou codificada, durante uma transmissão. Sua codificação pode ser feita de diferentes formas, sendo alguns exemplos:

• Com uma representação textual XML
• Com uma representação binária compacta little-endian ou big-endian, composta por números inteiros de 32 bits, caracteres ASCII ou UTF-8
• Com uma representação binária do tipo TLV (Type-Length-Value)
• Com uma representação textual em CSV ou JSON

Ambos conceitos são de grande importância no projeto de protocolos. A sintaxe abstrata especifica as estruturas de dados existentes nos intercâmbios realizados pelo protocolo. Essa especificação deve ser independente de arquitetura de computador ou linguagem de programação, podendo ser traduzida para uso em qualquer plataforma de hardware e/ou software, para que o protocolo possa ser usado nessas plataformas. A sintaxe concreta especifica como essas estruturas de dados devem ser codificadas para transmissão. Dessa forma, sistemas em comunicação podem estar em acordo quanto ao significado dos dados transmitidos. Dada sua importância, existem padrões para especificação de sintaxe abstrata e sintaxe concreta, sendo duas delas proeminentes:

• ASN.1 (Abstract Syntax Notation One): ASN.1 é uma linguagem de especificação de sintaxe abstrata definida pelo ITU-T. A sintaxe concreta está dissociada dessa linguagem, podendo ser realizada de diferentes formas, tais como BER (Binary Encoding Rules), PER (Packed Encoding Rules), XER (XML Encoding Rules) e outras. A notação ASN.1 não impõe uma escolha sobre qual codificação utilizar, ficando assim de livre escolha pelo desenvolvedor.
• ABNF (Augmented Backus-Naur Form): ABNF é uma notação definida pelo IETF para expressar tanto a sintaxe abstrata quanto sua codificação textual, sendo portanto voltada para estruturas de dados representadas em modo de texto. Assim, ABNF impõe também a codificação a ser usada nas mensagens.

... e algumas outras propostas por empresas ou grupos de desenvolvimento de software correndo por fora:

• Protocol-buffers: linguagem de especificação de sintaxe abstrata criada pelo Google. Possui suporte a várias linguagens de programação, como Java, Python e C++.
• MessagePack: define um formato de serialização binária para sintaxe concreta. Não possui uma notação para sintaxe abstrata: a serialização é feita diretamente a partir de valores representados na linguagem de programação alvo. Suporta muitas linguagens, tais como C, C++, Python e Java.

ASN.1

• Site oficial sobre ASN.1
• Introdução a ASN.1
• Um exemplo sobre ASN.1
• ASN.1: Communication between heterogeneous systems (livro gratuito)
• ASN.1 Complete (livro gratuito)
• Compilador ASN.1

De acordo com a Introdução a ASN.1, Abstract Syntax Notation number One é um padrão que define um formalismo para a especificação de tipos abstratos de dados. ASN.1 não é uma linguagem de programação, e sim uma notação para especificar tipos de dados.

A notação fornece um certo número de tipos básicos predefinidos, tais como:

• INTEGER: números inteiros
• BOOLEAN: valores booleanos
• IA5String, UniversalString, NumericString, PrintableString: cadeias de caracteres
• BIT STRING: cadeias de bits
• OBJECT IDENTIFIER: identificador de objeto

Ela torna possível a definição de tipos de dados, tais como:

• SEQUENCE: estruturas de dados (struct)
• SEQUENCE OF: listas
• CHOICE: escolha entre valores

Uma definição em ASN.1 pode ser mapeada para uma estrutura de dados em linguagem de programação como C, C++, Java e outras (Python, Perl, ...). Assim, essa estrutura de dados pode ser usada em software que implementa um protocolo. A codificação e decodificação entre essa estrutura de dados e os dados transmitidos e recebidos deve ser feita por meio de algoritmos disponibilizados em bibliotecas. Com isso, os dados em transmissão podem ser representados de diferentes maneiras, como TLV, XML e outras, independente da especificação da estrutura de dados.

A conversão da especificação em ASN.1 para uma linguagem de programação específica deve ser realizada com um compilador ASN.1. Existem ferramentas como essa para diversas linguagens, como C, C++ e Java (e mesmo Python). Em particular, existe um compilador ASN.1 gratuito capaz de traduzir as especificações para linguagem C, além de prover uma bilbioteca para codificação e decodificação.

O exemplo sobre a descrição de ativos pode ser usado para introduzir a linguagem ASN.1. A estrutura de dados Ativo pode ser especificada usando a declaração mostrada na coluna da esquerda. A estrutura de dados em linguagem C gerada pelo compilador ASN.1 está na coluna da direita:

ASN.1	Linguagem C
Module-Exemplo DEFINITIONS AUTOMATIC TAGS ::= BEGIN Ativo ::= SEQUENCE { nome PrintableString (SIZE(1..16)), codigo INTEGER, valor INTEGER, data NumericString(SIZE(8)), horario NumericString (SIZE(6)) } END	/* Ativo */ typedef struct Ativo { PrintableString_t nome; long codigo; long valor; NumericString_t data; NumericString_t horario; /* Context for parsing across buffer boundaries */ asn_struct_ctx_t _asn_ctx; } Ativo_t;

A documentação do compilador ASN.1 e uma demonstração de como escrever um programa que use uma API ASN.1 está aqui:

• Compilador ASN.1 e a API ASN1++

De forma alternativa, existem compiladores ASN.1 para outras linguagens de programação, como este:

• jASN.1: Compilador ASN.1 para Java

Atividade

1. Especifique as mensagens do vocabulário do seu protocolo usando ASN.1. Consulte o material de referência para identificar os tipos básicos e as declarações apropriadas para suas mensagens.
2. Compile sua especificação usando o Compilador ASN.1
3. Escreva dois programas de teste:
   • Um programa deve codificar as mensagens, gravando-as em um arquivo
   • O outro programa deve decodificá-las, carregando os dados do arquivo e transformando-os em instâncias das mensagens.

10/05: Projeto 2: ASN.1

Para exercitar o uso de ASN.1 para especificação da sintaxe do protocolo, a seguinte atividade deve ser realizada:

• Transmissão e recepção de mensagens: escreva um programa transmissor e outro receptor, os quais se comunicam por uma conexão TCP. O transmissor envia uma sucessão de mensagens, as quais devem ser decodificadas e apresentadas pelo receptor. Use as mensagens do seu protocolo de aplicação.

Revisão sobre sockets TCP

• Um tutorial resumido sobre sockets
• Outro tutorial mais completo (cópia no servidor de Tele) (versão original)

O uso sockets TCP usando a API de sockets pode ser resumida nos seguintes passos:

Cliente:

1. Criar um socket (socket)
2. Vinculá-lo a um endereço e port (bind)
3. Conectá-lo a um servidor (connect)
4. Enviar e receber dados (send, recv)
5. Encerrá-lo (close)

Servidor:

1. Criar um socket (socket)
2. Vinculá-lo a um endereço e port (bind)
3. Ativá-lo para que possa receber conexões (listen)
4. Receber conexão (accept) ... isso cria um novo socket automaticamente, através do qual se pode:
   1. Enviar e receber dados (send, recv)
   2. Encerrá-lo (close)
5. Encerrar o socket principal (close) ... isso impede a recepção de novas conexões, mas não encerra as conexões já aceitas e em andamento.

Exemplos existem nos tutoriais indicados nos links no início desta seção. Porém para facilitar o uso de sockets foram criadas algumas classes C++:

• Socket++: classes para uso simplificado de socket TCP e UDP (versão no github)

As classes são TCPClientSocket e TCPServerSocket. A descrição de suas interfaces está em TCPBaseSocket.h (ver comentários). Objetos dessas classes funcionam como sockets, porém com simplificações (não são necessários todos os passos da API de sockets do sistema operacional). Existe um exemplo de utilização nos arquivos client.cpp e server.cpp:

Exemplo de cliente

#include <cstdlib> #include <iostream> #include "TCPBaseSocket.h" using namespace std; /* * */ int main(int argc, char** argv) { TCPClientSocket client; // conecta no servidor da wiki (pode-se usar o nome DNS ou // o endereço IP do servidor) client.connect("wiki.sj.ifsc.edu.br", 80); // faz uma requisição HTTP client.send("GET / HTTP/1.1\n\n"); // recebe e mostra a resposta do servidor string resp = client.recv(10240); cout << resp << endl; return 0; }

Exemplo de servidor

#include <cstdlib> #include <iostream> #include "TCPBaseSocket.h" using namespace std; /* * */ int main(int argc, char** argv) { // cria um socket servidor que recebe conexões no port 8000 TCPServerSocket server(8000); // fica eternamente recebendo novas conexões // e dados de conexões existentes while (true) { try { // aguarda uma nova conexão ou dados em // uma conexão existente Connection & sock = server.wait(0); string addr; unsigned short port; // obtém o IP e port do socket da outra ponta da // conexão sock.get_peer(addr, port); // se for nova conexão, apenas mostra IP e port da outra ponta if (sock.isNew()) { cout << "Nova conexão: " << addr << ':' << port << endl; } else { // tenta receber até 1024 bytes no socket retornado // por "wait" string data = sock.recv(1024); // conseguiu ler algo desse socket ... if (data.size()) { // ...mostra-os na tela e envia-os de volta // para a outra ponta da conexão cout << "recebeu de " << addr << ':' << port; cout << ": " << data << endl; data = "recebido: " + data; sock.send(data); } } } catch (TCPServerSocket::DisconnectedException e) { // esta exceção informa que uma conexão foi encerrada // o socket correspondente foi invalidado automaticamente cout << e.what() << ": " << e.get_addr() << ':'; cout << e.get_port()<< endl; } } return 0; }

O diagrama de classes a seguir mostra as classes envolvidas:

... mas quem quiser tentar (ou conhecer) algo mais completo, pode experimentar a biblioteca Boost.Asio.

TAREFA

1. Crie dois programas: um deles gera mensagens de um protocolo hipotético, codifica-as com DER e envia-as por um socket TCP, e outro recebe mensagens codificadas de um socket TCP, decodifica-as e mostra-as na tela (apresenta primeiro o tipo de mensagem recebida seguido de seu conteúdo). Exemplo de especificação de mensagens:

Teste1 DEFINITIONS AUTOMATIC TAGS ::=
BEGIN

Mensagem ::= SEQUENCE {
  id INTEGER,
  nome PrintableString (SIZE(1..16))
}

END

... e de utilização:

demo.cc

#include <parser_Teste1.h> #include <iostream> #include <sstream> using namespace std; int main() { TMensagem pkt; pkt.set_id(1234); pkt.set_nome("manoel"); // verifica se os valores contidos na estrutura de dados respeitam // a especificação pkt.check_constraints(); // mostra a estrutura de dados na tela cout << "Estrutura de dados em memória (antes de codificação XER):" << endl; pkt.show(); // cria o codificador ostringstream out; TMensagem::XerSerializer encoder(out); // codifica a estrutura de dados encoder.serialize(pkt); cout << endl; cout << out.str() << endl; // cria o decodificador istringstream inp(out.str()); TMensagem::XerDeserializer decoder(inp); // tenta decodificar uma estrutura de dados TMensagem * other = decoder.deserialize(); cout << endl; if (other) { cout << "Estrutura de dados obtida da decodificação XER:" << endl; other->show(); } else cerr << "Erro: não consegui decodificar a estrutura de dados ..." << endl; // devem-se destruir explicitamente as estruturas de dados obtidas // do decodificador delete other; }

2. Estenda seu programa para que as mensagens possam ser de dois tipos:

Mensagem DEFINITIONS AUTOMATIC TAGS ::=
BEGIN

Login ::= SEQUENCE {
  usuario PrintableString (SIZE(1..12)),
  senha PrintableString (SIZE(4..12))
}

Dados ::= SEQUENCE {
  seq INTEGER,
  x INTEGER,
  y INTEGER
}

Mensagem ::= SEQUENCE {
  id INTEGER,
  msg CHOICE {
    inicio Login,
    dados Dados
  }
}
 
END

... e de utilização:

  TMensagem pkt;

  // define o valor do campo "id"
  pkt.set_id(8);

  // Acessa o campo choice, que será referenciado
  // pela variável "msg" (note o operador &)
  TMensagem::Choice_msg & msg = pkt.get_msg();

  // Dentro de "msg" acessa-se "inicio": isso faz
  // com que o campo choice contenha um valor do tipo
  // "Login" (não pode mais ser mudado).
  TLogin login = msg1.get_inicio();

  // define os valores dos campos de "inicio"
  login.set_usuario("aluno");
  login.set_senha("blabla...");

17/05: Projeto 2: ABNF

• RFC 5234: ABNF
• ABNF na Wikipedia

ABNF (Augmented Backus-Naur Form) é uma notação sintática definida pelo IETF para especificar mensagens de protocolos de aplicação da Internet. Ela é usada para especificar mensagens dos protocolos HTTP, SIP, SMTP, IMAP4, entre outros. ABNF possibilita especificar uma gramática para mensagens codificadas textualmente. Portanto, ela se aplica a protocolos cuja sintaxe concreta é uma representação em texto.

Um exemplo de especificação ABNF segue abaixo. Ela representa um endereço de e-mail no formato nome@algum.dominio:

email=trecho arroba 1*8(trecho ".") trecho
trecho=1*16ALPHA
arroba=%d64

Uma especificação ABNF é composta por uma ou mais regras. Cada regra possui um nome e uma declaração. No exemplo acima, há três regras: email, trecho e arroba. Cada regra é declarada da seguinte forma:

regra = elementos crlf

... sendo elementos formado por um ou mais nomes de regras ou valores terminais, e crlf corresponde à sequência \r\n (carriage return + newline). Um valor terminal corresponde a uma sequência de um ou mais caracteres (i.e. a uma string).

As regras de composição de regras estão descritas de forma sucinta na própria RFC 5234.

Compilador ABNF

• ABNF++: um gerador de parser ABNF

A geração de mensagens com base em uma gramática ABNF pode ser feita diretamente e de forma simples. Basicamente trata-se de gerar mensagens de texto compostas por valores devidamente representados. No entanto, o processo inverso é um pouco mais difícil. A identificação de mensagens recebidas, e a extração dos valores relevantes ali representados, evolve a utilização de um parser ABNF. Um parser é um programa que verifica um dado de entrada de acordo com uma gramática, decompondo esse dado de entrada em seus elementos de acordo com essa gramática.

Um parser ABNF deve ser capaz de seguir uma gramática ABNF qualquer, e usá-la para reconhecer e decompor mensagens. Usualmente se obtém um parser por meio de um gerador de parser, o qual gera um parser específico para uma dada gramática. O parser gerado é fornecido como código-fonte em alguma linguagem de programação. Existem alguns geradores de parser ABNF na Internet, tais como:

• APG
• parse2

... porém eles não se mostraram apropriados para uso na disciplina (ao menos não com C++). Sendo assim, foi desenvolvido um gerador de parser próprio chamado de ABNF++. Em sua página na wiki há a documentação sobre sua utilização.

Outras sintaxes/codificações

Além de ASN.1 e ABNF, que são padronizadas, existem outras formas de especificar, representar e codificar mensagens. Abaixo seguem algumas possibilidades:

• JSON (Javascript Object Notation): define uma notação para representar dados, podendo ser considerada a própria sintaxe concreta.
  • RFC 7159: The JavaScript Object Notation (JSON) Data Interchange Format
  • RapidJSON: um parser/gerador JSON para C++
• MessagePack: define uma codificação de dados (sintaxe concreta). Não oferece uma notação para representá-los independente de linguagem e plataforma.
• Protocol Buffers: define uma notação para especificar dados que guarda semelhanças com ASN.1. A parte de sintaxe concreta é predefinida.

Atividade

1. Experimente utilizar o gerador de parser para criar um parser para a gramática do exemplo apresentado no início da aula. Em seguida, teste-o com alguns endereços de e-mail.
2. O reconhecimento de URI é uma tarefa mais complexa. Crie um parser a partir desta gramática, e teste-o com diferentes URI.
3. Seu protocolo de aplicação poderia ser especificado com ABNF ? Compare a codificação das mensagens com ASN.1 e ABNF, considerando a facilidade para representação das informações e de utilização do esquema de codificação.

24/05: Projeto 2: especificação do protocolo

Cada equipe deve especificar seu protocolo, tendo em vista a implementação de um protótipo. A especificação inclui:

• o problema a ser resolvido (ou o objetivo do protocolo)
• o serviço a ser oferecido
• o ambiente de execução e o tipo de canal a ser usado
• o conjunto de mensagens do protocolo devidamente descritas
• o comportamento modelado como MEF

A especificação deve ser entregue via Moodle até dia 29/05:

• Tarefa: especificação do protocolo

O protótipo deve conter:

• Interfaces de programação a serem usadas pelos diferentes atores envolvidos, o que depende do modelo de comunicação adotado:
  • Cliente-servidor: APIs para cliente e para servidor
  • Publisher/subscriber: APIs para participantes (assinantes e publicadores) e para broker (caso exista)
  • P2P: API para participantes
• Implementação de referência do protocolo
• Aplicação de demonstração

31/05: Projeto 2: conclusão

• Prazo de entrega: 14/06/2017
• Entrega deve ser composta de um arquivo compactado contendo os arquivos do projeto
• Entrega deve ser feita pelo Moodle.

05/06: Verificação de protocolos

• Spin (código-fonte)
• The SPIN Model Checker (livro em formato CHM)
  • The SPIN Model Checker (versão em PDF)
• capítulo 5 do livro Design and Validation of Computer Protocols
• Um tutorial sobre SPIN

Um protocolo pode ser entendido como um conjunto de regras para interação de processos concorrentes. Um aspecto essencial de um protocolo é o conjunto de sequências de mensagens e ações permitidas. Por exemplo, no protocolo de enlace PTP as sequências a seguir são aceitáveis (prefixo C: identifica uma ponta do enlace, e S: a outra ponta):

• C:DATA_0, S:ACK_0, C:DATA_1, S:ACK_1
• C:DATA_0, S:ACK_0, S:DATA_0, C:ACK_0, C:DATA_1, C:DATA_1, S:ACK_1

... mas estas não:

• C:DATA_0, S:ACK_1, C:DATA_1, S:ACK_0
• C:DATA_0, S:DATA_0, C:ACK_0, S:ACK_0

As regras de procedimento devem manter sempre o estado do protocolo consistente em todas as entidades de protocolo envolvidas (no exemplo, tanto no cliente quanto no servidor). Isso não é simples de garantir, mesmo com protocolos de baixa complexidade. Tome-se o exemplo de um protocolo para transferência de sequências de caracteres por linhas analógicas, descrito na seção 2.3 do capítulo 2 do livro Design and Validation of Computer Protocols, chamado de protocolo Lynch.

O propósito do protocolo Lynch é transferir arquivos de texto como sequências de caracteres através e uma linha telefônica, com proteção contra erros, supondo que todos erros de transmissão possam ser detectados. Comunicações são full-duplex, e confirmações positivas e negativas são empregadas para implementar um mecanismo de garantia de entrega de mensagens. Cada mensagem possui duas partes: o dado transmitido e informações de controle que se aplica às transmissões em sentido reverso. Supõe-se que mensagens possam ser distorcidas, mas não perdidas, inseridas, duplicadas ou reordenadas, e que exista um módulo de mais baixo nível (ex: encoder/decoder) que transforme uma mensagem distorcida em uma mensagem especial do tipo err. O vocabulário do protocolo é formado por três mensagens:

• ack: composta por um dado e uma confirmação positiva do dado recebido previamente em sentido contrário.
• nak: composta por um dado e uma confirmação negativa do dado recebido previamente em sentido contrário.
• err: mensagem especial que representa uma mensagem recebida com erro.

As regras de procedimento desse protocolo são:

1. Se a recepção anterior foi livre de erros, a próxima mensagem no canal reverso deve incluir uma confirmação positiva. Se a recepção anterior possuir erro, deve-se incluir uma confirmação negativa.
2. Se a recepção anterior incluir uma confirmação negativa, ou a recepção anterior possuir erro, deve-se retransmitir a mensagem no canal reverso. Caso contrário, obtém-se uma nova mensagem para transmissão

Essas regras podem ser representadas por diferentes tipos de diagramas, dentre eles este diagrama SDL:

Diagrama SDL para o protocolo Lynch

Como se pode verificar se esse protocolo funciona a contento ? Em outras palavras, que ele possibilite a comunicação livre de erros entre duas entidades ? Antes de mais nada, deve-se definir o que se entende por funcionar a contento. No caso do protocolo Lynch, seu correto funcionamento pode ser expresso por estas propriedades:

• Garantia de entrega: toda mensagem enviada por uma entidade do protocolo no final das contas é recebida pela outra entidade do protocolo.
• Duplicatas descartadas: Mensagens duplicadas não são aceitas

Parece simples verificar se essas propriedades sempre valem a longo da operação do protocolo. O protocolo é de baixa complexidade, e isso aparentemente deve ser fácil de conferir.

Atividade

Verifique se as propriedades do protocolo Lynch sempre valem ...

Modelos para verificação

A verificação de propriedades de um protocolo envolve demonstrar que suas propriedades desejadas nunca são violadas. Existem diferentes técnicas para realizar esse tipo de verificação, tais como álgebra de processos, verificação de modelos e até mesmo simulação (se bem que esta última não é capaz de fornecer um veredito definitivo). Nesta disciplina será estudada a verificação de modelos, ou model checking, como é mais conhecida.

A verificação de modelos envolve a criação de um modelo que represente o sistema a ser verificado, a identificação de propriedades desejadas expressadas de acordo com esse modelo, e a busca automática e exaustiva por violações dessas propriedades. Assim, três elementos estão envolvidos:

1. Um modelo do comportamento do sistema, expressado segundo algum formalismo: tratando-se de um sistema a eventos discretos, um protocolo pode ser modelado de acordo com alguma construção matemática para sistemas de estados finitos. Máquinas de estados finitos se aplicam a essa necessidade, porém alguns incrementos em relação às máquinas de estados vistas anteriormente são necessários. Em particular, o modelo do sistema em que se aplica um protocolo envolve duas ou mais máquinas de estados que se comunicam. Isso pode ser descrito implicitamente por alguma linguagem de programação de propósito específico.
2. Um conjunto de propriedades desejadas do sistema: as propriedades correspondem a combinações de condições baseadas em atributos do modelo, ou sequências de eventos.
3. Uma ferramenta que automatize a busca exaustiva de violações de propriedades dentro do modelo: tal ferramenta deve explorar todas as possíveis sequências de eventos no modelo, verificando as propriedades desejadas a cada passo.

Para introduzir a verificação de modelos, um exercício sobre o protocolo Lynch será realizado. Mas antes é necessário conhecer uma linguagem de modelagem para verificação de sistemas e uma ferramenta de verificação que se baseie nessa linguagem.

A linguagem PROMELA e o verificador SPIN

A linguagem PROMELA (Process Meta-Language), conforme introduzida no capítulo 2 e melhor descrita no capítulo 3 do livro The SPIN Model Checker (PDF), é uma linguagem para modelagem de sincronização e coordenação de processos concorrentes. Sendo voltada para verificação de sistemas, essa linguagem não se aplica a expressar algoritmos em geral, tampouco calcular coisas. Seus elementos básicos são:

• Processos assíncronos
• Canais de mensagens bufferizados ou não
• Declarações de sincronização
• Dados estruturados

Intencionalmente não há noção de tempo, não existe um relógio a ser consultado, não existem números em ponto flutuante e há poucas funções computáveis. Esse desenho enxuto tornam a mdelagem de sistemas concorrentes relativamente simples com a linguagem (ao menos essa é a intenção). A execução e verificação de programas escritos em PROMELA se faz com um verificador de modelos chamado SPIN (Simple PROMELA Interpreter). Essa ferramenta possibilita executar modelos de forma a simulá-los ou a verificá-los exaustivamente.

A modelagem de sistemas envolve portanto a escrita de programas em PROMELA. Assim, a seguir se apresenta uma introdução sobre a linguagem com base em seus elementos básicos.

A instalação do SPIN deve seguir estes passos:

1. Instale os softwares bison e flex. No Ubuntu ou Debian isso se faz assim:

   sudo apt-get install bison flex
   

2. Obtenha o código-fonte do SPIN
3. Descompacte-o em algum diretório
4. A partir desse diretório, em um terminal entre em Spin/Src6.4.3
5. Execute o comando make
6. Ao final, o programa spin deve ter sido compilado.

Processos assíncronos

Um processo é declarado com a palavra-chave proctype, seguida de seu nome. O processo abaixo apresenta o famigerado hello world na saída padrão e em seguida termina.

active proctype hello() {
  printf("hello world: meu id é %d\n", _pid)
}

Para executá-lo, salve-o em um arquivo e em seguida execute-o usando o spin. Por exemplo, se o nome do arquivo que o contém for hello.pml, a execução com spin deve ser assim:

aluno@M2:~$ spin hello.pml
hello world: meu id é 0
1 process created

A palavra-chave active define que o processo deve ser executado assim que o programa iniciar. Uma vez terminado, a execução como um todo encerra, uma vez que nenhum processo permanceceu ativo. Um outro exemplo gera processos indefinidamente, e mostra como se pode iniciar um processo a partir de outro usando o comando run:

active proctype hello() {
  printf("hello world: meu id é %d\n", _pid)
  run hello()
}

Variáveis

Processos podem usar variáveis, cujos escopos podem ser locais ou globais. Variáveis são tipadas, e os tipos básicos são (mais detalhes ver capítulo 3 do livro The SPIN Model Checker:

• bit
• bool
• byte
• chan
• mtype
• pid
• short
• int
• unsigned

A declaração de variáveis é semelhante à de linguagem C, como se pode observar neste exemplo:

mtype = {ack, nak, err}

active proctype hello() {
  int x;
  pid p;
  mtype m = ack

  p = _pid;
  x = x + 1;
  printf("hello world: meu id é %d e x=%d\n", p, x)
  printf("... e m=")
  printm(m)
  printf("\n")
}

Tipos definidos

Podem-se definir tipos de dados de forma semelhante à declaração struct de linguagem C, usando-se a palavra-chave typedef:

typedef Mensagem {
  byte cod;
  int uid
}

active proctype teste() {
  Mensagem msg

  msg.cod = 111
  msg.uid = _pid
  printf("Mensagem: %d, %d\n", msg.cod, msg.uid)
}

.. o que pode ser conveniente para representar mensagens de um protocolo.

Canais de mensagens

Canais de mensagens são usados para modelar a troca de dados entre processos, e podem ser locais ou globais. Cada canal é declarado de forma a possibilitar mensagens de acordo de um determinado tipo, como neste exemplo:

typedef Mensagem = {
  pid uid;
  int cod
}

chan canal = [1] of {int}
chan outro = [8] of {Mensagem}
chan maisum = [0] of {int, byte}

No trecho de programa acima, são declarados três canais:

• canal: este canal transporta mensagens com do tipo int; ele possui uma fila com até 1 mensagem armazenada (enviada e ainda não recebida)
• outro: este canal transporta mensagens do tipo Mensagem, e possui uma fila com até 8 mensagens
• maisum: este canal transporta mensagens compostas por dois campos (int e byte), e não possui fila de mensagens. A ausência de fila implica a comunicação síncrona de processos: o transmissor bloqueia até que o receptor receba a mensagem

A comunicação por meio de um canal se faz com os comandos ! (envio) e ? (recepção), que devem ser usados desta forma:

chan canal1 = [1] of {int}
chan canal2 = [1] of {int, byte}

active proctype p1() {
  int msg
  byte codigo

  // envia uma mensagem pelo canal1
  canal1!9

  // aguarda uma mensagem pelo canal2
  canal2?msg,codigo

  printf("Recebeu %d,%d\n", msg, codigo)
}


active proctype p2() {
  int msg

  // envia uma mensagem pelo canal2
  canal2!2,15

  // aguarda uma mensagem pelo canal1
  canal1?msg

  printf("Recebeu %d\n", msg)
}

O envio é feito informando-se valores para cada campo do tipo de mensagem transportada pelo canal. Esses valores podem ser constantes ou fornecidos por variáveis. O envio não é bloqueante se houver espaço livre na fila do canal para mais uma mensagem. Se o canal estiver cheio, o envio causa o bloqueio do transmissor, mas isso pode ser mudado no Spin (ver seção sobre Message Channels do capítulo 3 do livro sobre o Spin). A recepção é sempre bloqueante, e segue uma sintaxe similar a da operação de envio. Logo após o comando e recepção ?, podem-se informar variáveis para armazenar o conteúdo da mensagem, ou especificar constantes. No segundo caso, a recepção somente é realizada se os valores das constantes forem iguais aos da mensagem a ser recebida através do canal.

Um exemplo simples e representativo é este modelo de um protocolo de bit alternado. Ele é composto por um processo transmissor e um receptor, os quais repetem indefinidamente uma sequência de mensagens. As mensagens se dividem em dados (msg0 e msg1) e confirmação (ack0 e ack1). O programa PROMELA para esse protocolo está a seguir:

mtype = { msg0, msg1, ack0, ack1 };
chan    to_sndr = [2] of { mtype };
chan    to_rcvr = [2] of { mtype };

active proctype Sender()
{
again:  to_rcvr!msg1;
        to_sndr?ack1;
        to_rcvr!msg0;
        to_sndr?ack0;
        goto again
}

active proctype Receiver()
{
again:  to_rcvr?msg1;
        to_sndr!ack1;
        to_rcvr?msg0;
        to_sndr!ack0;
        goto again
}

Executabilidade

Em PROMELA, uma sentença é executável ou não (bloqueável). A semântica de executabilidade de sentenças em PROMELA segue estas regras:

• atribuições e comandos do tipo print são sempre executáveis. Em outras palavras, nunca bloqueiam.
• envio de mensagens é executável se o canal não estiver cheio, do contrário é bloqueante
• recepção de mensagens é executável se houver mensagem no canal E se os valores nela contidos foram consistentes com os valores porventura especificados no comando de recepção
• expressões são executáveis se avaliarem para verdadeiro (true)

PROMELA define também um modelo de execução não-determinístico. Isso quer dizer que, se uma sequência apresentar uma bifurcação e ambos os ramos forem executáveis, um deles será sorteado para ser executado. Por exemplo:

chan canal1 = [1] of {int}
chan canal2 = [1] of {int}

active proctype p1() {
  int msg1, msg2

Repetir:

  if
  :: canal1?msg1 -> printf("Recebeu msg1=%d\n", msg1)
  :: canal2?msg2 -> printf("Recebeu msg2=%d\n", msg2)
  fi

  goto Repetir
}

active proctype p2() {
  denovo:

  if
  :: canal1!111
  :: canal2!222
  fi
  
  goto denovo
}

No processo p2 do exemplo acima, se somente canal1 tiver uma mensagem, a primeira sentença será executada. Se somente canal2 tiver uma mensagem, a segunda sentença será executada. E se ambos canais tiverem mensagens, qualquer uma das duas sentenças poderá ser executada. E o processo p1, por sua vez, fica indefinidamente enviando mensagens por ambos canais aleatoriamente.

Na estrutura de seleção if, uma sentença especial é dada pela palavra-chave else. Tal sentença é executável somente se nenhuma outra sentença do if for executável.

Repetição

O exemplo do processos transmissor p2 na seção anterior envolveu a repetição de transmissões pelos canais canal1 e canal2. A repetição foi controlada com o comando goto. Em PROMELA existe um comando específico para controlar a repetição. Ele possibilita reescrever o processo p2 daquele exemplo para que fique assim:

active proctype p2() {
  do
  :: canal1!111 -> printf("enviei pelo canal1\n")
  :: canal2!222 -> printf("enviei pelo canal2\n")
  od
}

Da mesma forma que a estrutura de seleção if, a estrutura de repetição do seleciona uma das sentenças executáveis de forma não-determinística. Se nenhuma sentença for executável, então do bloqueia. E, assim como no if, a sentença iniciada com else é executável se nenhuma outra sentença do mesmo bloco de repetição for executável. Por fim, o comando break possibilita interromper a repetição. O exemplo a seguir combina else e break: se não for possível enviar uma mensagem pelo canal1, tampouco pelo canal2, então a repetição é interrompida.

active proctype p2() {
  do
  :: canal1!111 -> printf("enviei pelo canal1\n")
  :: canal2!222 -> printf("enviei pelo canal2\n")
  :: else -> break
  od
}

Outra palavra-chave importante de PROMELA é timeout, cujo significado se assemelha a else. A diferença está no escopo: else é verdadeiro se nenhuma condição do bloco em questão for executável, e timeout é verdadeiro se nenhuma sentença de todos os processos do programa for executável.

Além de do .. od, pode-se usar for para repetir um bloco de sentenças com base em uma faixa de valores.

active proctype p2() {
  int x

  // envia 10 mensagens por canal1 ou canal2,
  // selecionando-os de forma não-determinística
  // os limites da faixa de valores podem ser expressões contendo
  // constantes ou variáveis
  for (x: 1..10) {
    if
    :: canal1!x -> printf("enviei %d pelo canal1\n", x)
    :: canal2!x -> printf("enviei %d pelo canal2\n", x)
    fi
  }
}

Seleção de valores

A seleção ou sorteio de valores pode ser feita com select, que escolhe um valor dentre uma faixa:

proctype teste() {
  int x = 0

  // seleciona um valor entre 1 e 20 e armazena-o em x
  // sai do laço quando x >= 10
  // os limites da faixa devem se expressões contendo somente constantes
  do
  :: x < 10 -> select(x : 1 .. 20)
     printf("%d -> x=%d\n", _pid, x)
  :: else -> break
  od
}

Como gerar um verificador com SPIN

Os exemplos anteriores mostram como simular modelos escritos em PROMELA. A verificação desses modelos envolve a criação de um verificador, o que deve ser feito desta forma:

1. Execute o spin instruindo-o a gerar um verificador:

   ./spin -a modelo.pml
   

2. O comando anterior deve gerar um arquivo de programa pan.c. Compile-o com este comando:

   gcc -o pan pan.c
   

3. Execute o verificador:

   ./pan
   

4. Pode-se executar o verificador de formas alternativas. Por exemplo, para buscar ciclos sem progresso no modelo:

   ./pan -l
   

5. Outras opções do verificador podem ser vistas com:

   ./pan -h
   

Atividade

1. Escreva um modelo para o problema do produtor e consumidor. Suponha que o produtor produza 10 mensagens e depois termine, e o buffer intermediário tenha capacidade para 4 mensagens.
2. Modifique seu modelo da questão anterior para que existam 2 produtores.
3. Escreva um modelo para o problema dos filósofos glutões, supondo a existência de 5 filósofos. Verifique se seu modelo é livre de deadlock.
4. Escreva um modelo para um protocolo do tipo pare-e-espere em um ambiente de execução livre de erros.
5. Escreva um modelo para um protocolo do tipo pare-e-espere em um ambiente de execução em que erros são possíveis ... seu modelo deve prever a perda de mensagens, retransmissões e descarte de mensagens duplicadas.
6. Crie um modelo para o protocolo Lynch e use-o para verificar se esse protocolo é livre de erros.
7. Escreva um modelo para um protocolo que faça autenticação de usuário: a entidade cliente deve conseguir se autenticar na entidade servidora antes de poder enviar e receber mensagens de dados.
8. Escreva um modelo para o enquadramento que foi implementado no protocolo ponto-a-ponto.

Modelos para o protocolo pare-espere
Modelos implementam esta MEF

14/06: Verificação do protocolo

Hoje continuaremos o estudo da verificação de modelos com PROMELA e SPIN. O resumo a seguir foi escrito a partir do capítulo 4 do livro The SPIN Model Checker, e o capítulo 6 do livro Design and Validation of Computer Protocols.

Verificação de propriedades

Do ponto de vista de um sistema distribuído ou concorrente, podem-se identificar dois requisitos para a correção de um sistema:

• Segurança (safety): segurança diz respeito ao que não deve ser possível ocorrer no sistema, ou ao conjunto de propriedades que não podem ser violadas. Isso inclui estados que nunca devem ser alcançados, ou sequências de estados as quais não podem ocorrer.
• Vivacidade (liveness): vivacidade diz respeito ao que sempre deve valer para o sistema, ou ao conjunto de propriedades que sempre devem ser satisfeitas.

Para fins de verificação de propriedades, PROMELA/SPIN definem dois tipos de reivindicações de correção:

• alcançabilidade: esse tipo de reivindicação se baseia em estados alcançáveis ou inalcançáveis. Isso também se chama propriedades de estado.
• factibilidade: esse outro tipo de reivindicação se baseia na executabilidade ou não de sequências de estados. Isso também é chamado de propriedades de caminho.

Verificação de condições (assertions)

A verificação de uma condição pode ser feita com o comando assert. Esse comando verifica se uma expressão avalia para verdadeiro e, caso contrário, interrompe a execução do programa. Isso pode ser usado para a verificação pontual de uma propriedade do sistema.

active proctype p1() {
  int msg
  int n1 = 0
  int n2 = 0

  do
  :: canal1?msg -> n1++; assert(n1 < 10)
  :: canal2?msg -> n2++; assert(n2 < 15)
  od
}

No exemplo acima, o processo p1 aceita que sejam recebidas no máximo 10 mensagens pelo canal1 e 15 mensagens pelo canal2.

Para verificar condições em um modelo, deve-se compilá-lo da seguinte forma:

# opção -a: usada para gerar um verificador, que estará no arquivo pan.c
./spin -a djikstra.pml

# Compila o verificador, que será o programa "pan"
gcc -o pan pan.c

# Executa o verificador
./pan

Meta-rótulos (meta labels)

Três tipos especiais de rótulos podem ser inseridos em um programa para orientar o verificador a identificar certos estados no sistema:

• end: rótulos com prefixo end marcam estados finais de um processo. Inicialmente, o estado final de um processo é criado implicitamente na chave final de sua declaração }. Porém há situações em que um processo nunca termina, porém isso não se configura um erro. Assim, rótulos end possibilitam informar que outros estados do processo são finais.
• progress: rótulos com prefixo progress informam que certos estados, se visitados, indicam que um processo está progredindo sua execução. Em outras palavras, que a execução não está presa em algum laço indefinidamente.
• accept: rótulos com prefixo accept marcam estados que não devem ser visitados infinitamente frequente. Isso pode ser usado para identificar ciclos de visitação de estados os quais não devem ocorrer indefinidamente.

O exemplo a seguir mostra o uso de um rótulo end, em um modelo sobre semáforos. O processo Djikstra nunca termina, pois ele implementa um semáforo e deve estar sempre disponível para atender pedidos de entrada em seção crítica. Assim, o estado em que inicia a verificação do semáforo é um estado final.

mtype { p, v };
chan sema = [0] of { mtype };
active proctype Dijkstra()
{       byte count = 1;
end:    do
        :: (count == 1) ->
                sema!p; count = 0
        :: (count == 0) ->
                sema?v; count = 1
        od
}
active [3] proctype user()
{       do
        :: sema?p;        /* enter */
critical: skip;           /* leave */
          sema!v;
        od
}

Uma pequena alteração no exemplo demonstra o uso de um rótulo progress. Neste caso, marca-se o estado em que se libera o semáforo como sendo um estado indicador de progresso. Se o processo Djikstra passar frequentemente por esse estado, o verificador conclui que o processo está em progresso.

active proctype Dijkstra()
{       byte count = 1;
end:    do
        :: (count == 1) ->
progress:       sema!p; count = 0
        :: (count == 0) ->
                sema?v; count = 1
        od
}

Por fim, para buscar ciclos sem progresso de um modelo deve-se usar a opção -l do verificador:

./spin -a djikstra.pml
gcc -o pan pan.c  -DNP
./pan -l

Para buscar ciclos com estados accept de um modelo deve-se usar a opção -a do verificador:

./spin -a djikstra.pml
gcc -o pan pan.c  -DNP
./pan -a

Atividade

Para exercitar a verificação de protocolos, faça o seguinte:

1. Verifique os modelos para o problema do produtor e consumidor, de forma que:
   • Toda mensagem produzida seja efetivamente consumida
   • Toda mensagem deva ser consumida uma única vez
2. Verifique o modelo para o problema dos filósofos glutões, supondo a existência de 5 filósofos, de forma que:
   • Não exista deadlock
   • Nenhum filósofo morra de fome
3. Verifique o modelo para um protocolo do tipo pare-e-espere em um ambiente de execução em que erros são possíveis, tais como perdas de mensagens (tanto dados quanto ack). As seguintes propriedades devem ser verificadas:
   • Toda mensagem transmitida é entregue em algum momento futuro
   • Toda mensagem recebida é consumida uma única vez
   • Ausência de deadlock
   • Ausência de livelock
4. Verifique o modelo para um protocolo que faça autenticação de usuário, de forma que:
   • Mensagens são transmitida somente após cliente autenticado
   • Mensagens recebidas são aceitas apenas após cliente autenticado
5. Verifique o modelo para o enquadramento que foi implementado no protocolo ponto-a-ponto, de forma que:
   • Quadros com erros de CRC são descartados
   • Flags aparecem somente como delimitadores de quadro
   • Não há byte especial dentro de um quadro, a não ser que seja um ESC
   • Perda de sincronismo acarreta descarte de bytes recebidos
6. Verifique o protocolo Lynch quanto:
   • não duplicidade de mensagens
   • ausência de deadlock
   • ausência de livelock
7. Modele o protocolo de enlace sem-fio PTP, identifique critérios de correção e faça sua verificação.

19/06: Verificação de protocolos: lógica temporal

• Manual LTL para Spin
• Introdução a LTL no Spin
• Métodos formais e Lógica Temporal

Lógica clássica é boa para descrever um mundo estático, mas sistemas computacionais são dinâmicos. A lógica temporal é uma categoria de formalismos que procura descrever como as propriedades de um sistema variam com o tempo, porém sem se referir explicitamente ao tempo. As propriedades que tipicamente são verificadas com lógica temporal são:

• Segurança (safety): nada de ruim irá acontecer. Ex: não há deadlock, não ocorrem violações de exclusão mútua, mensagens duplicadas não são entregues.
• Vivacidade (liveness): algo de bom vai ocorrer. Ex: um programa fatalmente irá terminar, uma mensagem transmitida será corretamente recebida em algum momento futuro.
• Justiça (fairness): sistemas independentes progridem. Ex: se o meio de transmissão estiver frequentemente disponível, uma entidade de protocolo no final das contas conseguirá transmitir uma mensagem.

A lógica temporal introduz operadores temporais, usados para descrever a dinâmica de sistemas ao longo do tempo. Curiosamente, o tempo não aparece explicitamente em expressões formadas com esses operadores. Para fins de nosso estudo, será considerado um tempo linear, com um único caminho de execução (a alternativa é um tempo ramificado, em que múltiplos caminhos de execução são levados em conta). Ambas abordagens pressupõem um sistema modelado como um sistema de transições com rótulos (LTS - labeled transition system), como, por exemplo, máquinas de estados finitos. Cada passo de um caminho de execução é definido por um conjunto de proposições primitivas que avaliam para verdadeiro. Exemplos de proposições são:

• msg_tx: mensagem foi transmitida
• inCS_A: processo A está executando em uma seção crítica
• x == 0: variável x tem valor 0
• proc@label: processo proc está executando linha identificada pelo rótulo label

Sendo assim, um estado S é definido pelas proposições que são verdadeiras nesse estado.

Operadores temporais

Os operadores temporais se aplicam a estados, considerando uma sequência de estados. Tomando-se as fórmulas de lógica temporal f e g:

• Xf: f é verdadeiro no próximo estado (next f)
• Gf: f é verdadeiro em todos os estados (always f)
• Ff: f é verdadeiro em algum estado futuro (eventually f)
• fUg: g é verdadeiro em algum estado futuro, e f é verdadeiro em cada estado até então (f until g)

Outra notação:

• G: $\square$
• F: $\diamondsuit$
• X: $\bigcirc$

Dado o conjunto de proposições P, e fórmulas LTL f e g, as fórmulas LTL podem ser formadas com estas regras:

• p (uma proposição $p\in P$)
• Operadores booleanos:
  • $\neg f$: not f
  • $f\vee g$: f or g
  • $f\wedge g$: f and g
  • $f\implies g$: f implies g
• Operadores temporais:
  • $\bigcirc f$
  • $\square f$
  • $\diamondsuit f$
  • f U g

Uma outra forma de visualizar esses operadores temporais está ilustrada a seguir:

Algumas identidades entre fórmulas com esses operadores são:

• $\square f\Leftrightarrow \neg (\diamondsuit \neg f)$ ... $\diamondsuit f\Leftrightarrow \neg (\square \neg f)$
• $\square \square f\Leftrightarrow \square f$, $\diamondsuit \diamondsuit f\Leftrightarrow \diamondsuit f$
• $\diamondsuit f\Leftrightarrow trueUf$, $\square f\Leftrightarrow \neg (trueU\neg f)$
• f W g$\Leftrightarrow fUg\vee f$

Propriedades distributivas:

• $\square (f\wedge g)\Leftrightarrow \square f\wedge \square g$
• $\diamondsuit (f\vee g)\Leftrightarrow \diamondsuit f\vee \diamondsuit g$
• $\bigcirc (fUg)\Leftrightarrow (\bigcirc f)U(\bigcirc g)$
• $\bigcirc (f\vee g)\Leftrightarrow (\bigcirc f)\vee (\bigcirc g)$
• $\bigcirc (f\wedge g)\Leftrightarrow (\bigcirc f)\wedge (\bigcirc g)$

Exemplo de uso

Um primeiro exemplo pode ser aplicado ao caso de exclusão mútua entre processos. Supondo que inCS_X signifique processo X está na seção crítica, as seguintes proposições podem ser definidas:

1. Processos A e B nunca estão na seção crítica ao mesmo tempo:
   • $\square (\neg inCS_{A}\vee \neg inCS_{B})$
2. Nenhum dos processos monopoliza a seção crítica:
   • $\square (inCS_{A}\implies \diamondsuit \neg inCS_{A})$
   • $\square (inCS_{B}\implies \diamondsuit \neg inCS_{B})$

LTL e Spin

O verificador spin é capaz de verificar fórmulas LTL. As proposições primitivas podem ser:

Proposição primitiva	Exemplo
expressões baseadas em variáveis globais	(x == 0)
rótulos de processos	p1@inicio (rótulo inicio do processo p1) p1[2]@inicio (rótulo inicio do processo p1 com pid 2)
variáveis locais de processos	p1:x (variável local x do processo p1) p1[2]:x (variável local x do processo p1 com pid 2)

Os operadores temporais suportados são (OBS: note a falta do operador next):

Operador LTL no Spin	Operador LTL
[]	$\square$ (always)
<>	$\diamondsuit$ (eventually)
U	U (until)
&&	$\wedge$
||	$\vee$
->	$\implies$
<->	$\Leftrightarrow$

Variáveis e funções predefinidas que podem ser úteis:

• _pid: variável local que contém o PID de um processo
• _last: variável global que contém o PID do processo que contém a última sentença executada
• enabled(pid): função global que retorna true se existe ao menos uma sentença executável no processo identificado por pid

Para declarar fórmulas LTL em um modelo Promela, basta acrescentá-las ao final do arquivo com esta sintaxe:

ltl nome1 { formula 1}
ltl nome2 { formula 2}
...
ltl nomeN { formula N}

A geração do verificador deve ser feita com estes comandos:

spin -a modelo.pml
gcc -o pan pan.c

Por fim, a execução do verificador se faz assim:

./pan -a

Atividades

1. Para o sistema descrito no modelo Promela a seguir, verifique se o contador atinge o valor 10:

int count;
bool incr;

active proctype counter() {
  do
  :: incr -> count++
  od
}

active proctype env() {
  do
  :: incr = false
  :: incr = true
  od
}

Fórmula LTL
ltl ok { ([] <> (_last == 0)) -> <> (count == 10) }

2. Para o sistema do exercício 1, verifique também se a execução dos processos possui a propriedade da justiça: ambos os processos devem executar infinitamente frequente. Dica: lembre das variáveis e funções predefinidas do Spin.

Fórmulas LTL
// versão do professor ltl justica1 { ([] enabled(0) -> (<> (_last == 0))) && ([] enabled(1) -> (<> (_last == 1))) } // versão do André, Gabriel e Maria Luiza ltl justica2 { ([](_last == 0) -> (<> (_last == 1))) && ([](_last == 1) -> (<> (_last == 0))) }

3. Seja um protocolo ARQ do tipo pare-espere, em que processo p1 envia mensagens para processo p2 por um canal não confiável:

• Defina sentA para expressar se processo p1 recém enviou mensagem A, e recA se processo p2 recém recebeu mensagem A. Defina também sentB e recB da mesma forma.
• Defina loss para expressar se canal perdeu última mensagem

Sendo assim, verifique estas propriedades:

• Se uma mensagem for transmitida, ela será recebida em algum momento
• Se uma mensagem for recebida, ela foi previamente transmitida

Por fim, escreva esse modelo Promela, declare as fórmulas LTL, e verifique seu modelo.

4. Aplique a verificação com LTL aos problemas propostos aula passada ...

28/06: Conclusão

A conclusão da etapa 3 é a verificação do ARQ e MAC do protocolo do projeto 1. Isso tem por objetivos verificar se:

1. Esse componente está livre de deadlock e livelock
2. Um quadro transmitido é entregue em algum momento futuro
3. Quadros duplicados são devidamente descartados
4. Somente um nodo transmite a cada vez

A verificação deve se basear no protocolo implementado no projeto 1. Asism, o modelo Promela deve ser fiel ao comportamento do protocolo tal qual efetivamente desenvolvido.

A entrega dessa avaliação deve ser composta de:

1. Modelo escrito em Promela, junto com os recursos usados para verificação (fórmulas LTL, meta-rótulos). O modelo deve estar devidamente documentado e comparado ao código-fonte original do componente ARQ do protocolo do projeto 1.
2. Um relatório que mostre como cada propriedade foi verificada, e o resultado da verificação.

• Formulário para entrega no Moodle