Add more TCP constants

This commit is contained in:
Guillaume Cluzel
2020-08-04 12:22:44 +02:00
parent 7e7333f0cd
commit f051aa400e
8 changed files with 92 additions and 25 deletions

View File

@@ -1,2 +1,11 @@
-- Number of sockets that can be opened simultaneously
SOCKET_MAX_COUNT := 10
-- Default buffer size for reception
TCP_DEFAULT_RX_BUFFER_SIZE := 2860
-- Default buffer size for transmission
TCP_DEFAULT_TX_BUFFER_SIZE := 2860
-- Default SYN queue size for listening sockets
TCP_DEFAULT_SYN_QUEUE_SIZE := 4

View File

@@ -3,6 +3,21 @@ List of Options
The following table lists all the options allowed in the configuration file.
| **Option** | **Description** | **Range** |
|--------------------|-----------------------------------------------------|------------|
| `SOCKET_MAX_COUNT` | Number of sockets that can be opened simultaneously | `Positive` |
Socket Options
--------------
| **Option** | **Description** | **Range** | **Default** |
|--------------------|-----------------------------------------------------|------------|-------------|
| `SOCKET_MAX_COUNT` | Number of sockets that can be opened simultaneously | `Positive` | 16 |
TCP Options
-----------
| **Option** | **Description** | **Range** | **Default** |
|--------------------------|-----------------------------------------------------|------------------------|-------------|
| `TCP_MAX_RX_BUFFER_SIZE` | Maximum acceptable size for the receive buffer | 536 .. `Positive'Last` | 22_880 |
| `TCP_DEFAULT_RX_BUFFER_SIZE` | Default buffer size for reception | 536 .. `TCP_MAX_RX_BUFFER_SIZE` | 2_860 |
| `TCP_MAX_TX_BUFFER_SIZE` | Maximum acceptable size for the send buffer | 536 .. `Positive'Last` | 22_880 |
| `TCP_DEFAULT_TX_BUFFER_SIZE` | Default buffer size for transmission | 536 .. `TCP_MAX_TX_BUFFER_SIZE` | 2_860 |
| `TCP_MAX_SYN_QUEUE_SIZE` | Maximum SYN queue size for listening sockets | 1 .. `Positive'Last` | 16 |
| `TCP_DEFAULT_SYN_QUEUE_SIZE` | Default SYN queue size for listening sockets | 1 .. `TCP_MAX_SYN_QUEUE_SIZE` | 4 |

View File

@@ -1,6 +1,9 @@
project Prove is
for Source_Dirs use ("src/**");
for Source_Dirs use (".", "src/**");
Package Compiler is
for default_switches ("Ada") use ("-gnat2020");
for default_switches ("Ada") use
("-gnat2020",
"-I" & Prove'Project_Dir,
"-gnatep=" & Prove'Project_Dir & "prep.data");
end Compiler;
end Prove;

View File

@@ -128,15 +128,16 @@ is
Sock.n := 0;
Sock.recover := 0;
Sock.txBuffer.chunkCount := 0;
Sock.txBufferSize := 2_860;
Sock.txBufferSize := TCP_DEFAULT_TX_BUFFER_SIZE;
Sock.rxBuffer.chunkCount := 0;
Sock.rxBufferSize := 2_860;
Sock.rxBufferSize := TCP_DEFAULT_RX_BUFFER_SIZE;
Sock.retransmitQueue := System.Null_Address;
Sock.retransmitCount := 0;
Sock.synQueue := null;
pragma Annotate (GNATprove, False_Positive,
"memory leak might occur", "Memory should already be free");
Sock.synQueueSize := 0;
-- Limit the number of pending connections
Sock.synQueueSize := TCP_DEFAULT_SYN_QUEUE_SIZE;
Sock.wndProbeCount := 0;
Sock.wndProbeInterval := 0;
Sock.sackPermitted := False;

View File

@@ -166,7 +166,7 @@ is
retransmitCount : unsigned;
synQueue : Tcp_Syn_Queue_Item_Acc;-- Tcp_Syn_Queue_Item_Acc;
synQueueSize : unsigned;
synQueueSize : Syn_Queue_Size;
wndProbeCount : unsigned;
wndProbeInterval : Systime;

View File

@@ -186,10 +186,11 @@ is
-- Set the size of the SYN queue Limit the number of pending connections
if Backlog > 0 then
Sock.synQueueSize := unsigned'Min (Backlog, TCP_MAX_SYN_QUEUE_SIZE);
else
Sock.synQueueSize :=
unsigned'Min (TCP_DEFAULT_SYN_QUEUE_SIZE, TCP_MAX_SYN_QUEUE_SIZE);
Syn_Queue_Size(
unsigned'Min (Backlog, unsigned(TCP_MAX_SYN_QUEUE_SIZE)));
else
Sock.synQueueSize := TCP_DEFAULT_SYN_QUEUE_SIZE;
end if;
-- Place the socket in the listening state

View File

@@ -6,11 +6,58 @@ with System; use System;
package Tcp_Type with SPARK_Mode is
TCP_MAX_SYN_QUEUE_SIZE : constant unsigned := 16;
TCP_DEFAULT_SYN_QUEUE_SIZE : constant unsigned := 4;
type Syn_Queue_Size_Max is range 1 .. Natural'Last
with Size => unsigned'Size;
TCP_MAX_RX_BUFFER_SIZE : constant unsigned_long := 22_880;
TCP_MAX_TX_BUFFER_SIZE : constant unsigned_long := 22_880;
-- Maximum SYN queue size for listening sockets
#if TCP_MAX_SYN_QUEUE_SIZE'Defined then
TCP_MAX_SYN_QUEUE_SIZE : constant Syn_Queue_Size_Max := $TCP_MAX_SYN_QUEUE_SIZE;
#else
TCP_MAX_SYN_QUEUE_SIZE : constant Syn_Queue_Size_Max := 16;
#end if;
type Syn_Queue_Size is range 1 .. TCP_MAX_SYN_QUEUE_SIZE
with Size => unsigned'Size;
-- Default SYN queue size for listening sockets
#if TCP_DEFAULT_SYN_QUEUE_SIZE'Defined then
TCP_DEFAULT_SYN_QUEUE_SIZE : constant Syn_Queue_Size := $TCP_DEFAULT_SYN_QUEUE_SIZE;
#else
TCP_DEFAULT_SYN_QUEUE_SIZE : constant Syn_Queue_Size := 4;
#end if;
subtype Buffer_Size is Natural range 536 .. Natural'Last;
-- Maximum acceptable size for the receive buffer
#if TCP_MAX_RX_BUFFER_SIZE'Defined then
TCP_MAX_RX_BUFFER_SIZE : constant Buffer_Size := $TCP_MAX_RX_BUFFER_SIZE;
#else
TCP_MAX_RX_BUFFER_SIZE : constant Buffer_Size := 22_880;
#end if;
-- Maximum acceptable size for the send buffer
#if TCP_MAX_TX_BUFFER_SIZE'Defined then
TCP_MAX_TX_BUFFER_SIZE : constant Buffer_Size := $TCP_MAX_TX_BUFFER_SIZE;
#else
TCP_MAX_TX_BUFFER_SIZE : constant Buffer_Size := 22_880;
#end if;
type Tx_Buffer_Size is range 1 .. TCP_MAX_TX_BUFFER_SIZE;
type Rx_Buffer_Size is range 1 .. TCP_MAX_RX_BUFFER_SIZE;
-- Default buffer size for reception
#if TCP_DEFAULT_RX_BUFFER_SIZE'Defined then
TCP_DEFAULT_RX_BUFFER_SIZE : constant Rx_Buffer_Size := $TCP_DEFAULT_RX_BUFFER_SIZE;
#else
TCP_DEFAULT_RX_BUFFER_SIZE : constant Rx_Buffer_Size := 2_860;
#end if;
-- Default buffer size for transmission
#if TCP_DEFAULT_TX_BUFFER_SIZE'Defined then
TCP_DEFAULT_TX_BUFFER_SIZE : constant Tx_Buffer_Size := $TCP_DEFAULT_TX_BUFFER_SIZE;
#else
TCP_DEFAULT_TX_BUFFER_SIZE : constant Tx_Buffer_Size := 2_860;
#end if;
TCP_DEFAULT_MSS : constant unsigned_short := 536;
TCP_MAX_MSS : constant unsigned_short := 1_430;
@@ -82,9 +129,6 @@ package Tcp_Type with SPARK_Mode is
type Chunk_Desc_Array is array (0 .. 14) of Chunk_Desc
with Object_Size => 15 * (32 + System.Word_Size);
type Tx_Buffer_Size is range 1 .. TCP_MAX_TX_BUFFER_SIZE;
type Rx_Buffer_Size is range 1 .. TCP_MAX_RX_BUFFER_SIZE;
type Tcp_Tx_Buffer is record
chunkCount : unsigned;
maxChunkCound : unsigned;

View File

@@ -123,12 +123,6 @@
//TCP support
#define TCP_SUPPORT ENABLED
//Default buffer size for transmission
#define TCP_DEFAULT_TX_BUFFER_SIZE (1430*2)
//Default buffer size for reception
#define TCP_DEFAULT_RX_BUFFER_SIZE (1430*2)
//Default SYN queue size for listening sockets
#define TCP_DEFAULT_SYN_QUEUE_SIZE 4
//Maximum number of retransmissions
#define TCP_MAX_RETRIES 5
//Selective acknowledgment support