diff --git a/Makefile b/Makefile index c2cd8cd..565de51 100644 --- a/Makefile +++ b/Makefile @@ -428,6 +428,7 @@ clean: rm -f $(RESULT).hex rm -f $(RESULT).lst rm -f $(OBJ_DIR)/*.o + rm -r ./src/spark_config.h .PHONY: prove prove: prove.gpr $(wildcard ./src/ada/*.adb) $(wildcard ./src/ada/*.ads) diff --git a/options.md b/options.md index e345387..64642cc 100644 --- a/options.md +++ b/options.md @@ -20,4 +20,11 @@ TCP Options | `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 | \ No newline at end of file +| `TCP_DEFAULT_SYN_QUEUE_SIZE` | Default SYN queue size for listening sockets | 1 .. `TCP_MAX_SYN_QUEUE_SIZE` | 4 | +| `TCP_MAX_MSS` | Maximum segment size | 536 .. `Short_Integer'Last` | 1430 | +| `TCP_MIN_MSS` | Mimimum acceptable segment size | 1 .. `Short_Integer'Last` | 64 | +| `TCP_DEFAULT_MSS` | Default SYN queue size for listening sockets | 1 .. `TCP_MAX_MSS` | 536 | +| `TCP_MAX_RTO` | Maximum retransmission timeout | 1000 .. `unsigned'Last` | 536 | +| `TCP_MIN_RTO` | Minimum retransmission timeout | 100 .. `TCP_MAX_RTO` | 536 | +| `TCP_DEFAULT_MSS` | Initial retransmission timeout | 1 .. `TCP_MAX_RTO` | 536 | +| `TCP_INITIAL_WINDOW` | Size of the congestion window after the three-way handshake is completed | 1 .. 20 | 3 | diff --git a/src/ada/net_mem.ads b/src/ada/net_mem.ads index d7b6ba0..1c4eb50 100644 --- a/src/ada/net_mem.ads +++ b/src/ada/net_mem.ads @@ -3,6 +3,13 @@ with System; package Net_Mem is + -- Size of the buffers +#if NET_MEM_POOL_BUFFER_SIZE'Defined then + NET_MEM_POOL_BUFFER_SIZE : constant Positive := $NET_MEM_POOL_BUFFER_SIZE; +#else + NET_MEM_POOL_BUFFER_SIZE : constant Positive := 1536; +#end if; + type Chunk_Desc is record address : System.Address; length : unsigned_short; diff --git a/src/ada/net_mem_interface.ads b/src/ada/net_mem_interface.ads index 10b71ce..a120d8a 100644 --- a/src/ada/net_mem_interface.ads +++ b/src/ada/net_mem_interface.ads @@ -31,7 +31,7 @@ is Convention => C, External_Name => "memPoolFree", Global => null; - + procedure Mem_Pool_Free (Queue_Item : in out Tcp_Syn_Queue_Item_Acc) with diff --git a/src/ada/os_types.ads b/src/ada/os_types.ads index 8f9ff69..deb1502 100644 --- a/src/ada/os_types.ads +++ b/src/ada/os_types.ads @@ -7,7 +7,7 @@ package Os_Types is end record with Convention => C; - + type Os_Event_Acc is access Os_Event; -- This record type is consistant with the OsMutex type for freertos diff --git a/src/ada/socket_interface.adb b/src/ada/socket_interface.adb index b229319..b5d9eb6 100644 --- a/src/ada/socket_interface.adb +++ b/src/ada/socket_interface.adb @@ -101,8 +101,8 @@ is Sock.owned_Flag := False; Sock.closed_Flag := False; Sock.reset_Flag := False; - Sock.smss := 0; - Sock.rmss := 0; + Sock.smss := TCP_DEFAULT_MSS; + Sock.rmss := TCP_DEFAULT_MSS; Sock.iss := 0; Sock.irs := 0; Sock.sndUna := 0; diff --git a/src/ada/socket_types.ads b/src/ada/socket_types.ads index c742e6c..e8456c9 100644 --- a/src/ada/socket_types.ads +++ b/src/ada/socket_types.ads @@ -80,7 +80,7 @@ is SOCKET_IP_PROTO_TCP => 6, SOCKET_IP_PROTO_UDP => 17, SOCKET_IP_PROTO_ICMPV6 => 58); - + ------------------------ -- Receive queue item -- ------------------------ @@ -125,8 +125,8 @@ is closed_Flag : Bool; reset_Flag : Bool; - smss : unsigned_short; - rmss : unsigned_short; + smss : Mss_Size; + rmss : Mss_Size; iss : unsigned; irs : unsigned; @@ -183,7 +183,7 @@ is -- UDP specific variables receiveQueue : Socket_Queue_Item_Acc; end record - with + with Convention => C, Predicate => Socket_Struct.S_Event_Mask = SOCKET_EVENT_TIMEOUT or else @@ -212,7 +212,7 @@ is SOCKET_FLAG_DELAY : constant Socket_Flags := 16#8000#; -- Number of sockets that can be opened simultaneously - + #if SOCKET_MAX_COUNT'Defined then SOCKET_MAX_COUNT : constant Positive := $SOCKET_MAX_COUNT; #else @@ -301,7 +301,7 @@ is S_Remote_Port => Sock.S_Remote_Port )) with Ghost; - + -- The transition relation function is used to compute all the transitions -- that can happen when a message is received. diff --git a/src/ada/tcp_interface.adb b/src/ada/tcp_interface.adb index aa41c14..fa6f1cd 100644 --- a/src/ada/tcp_interface.adb +++ b/src/ada/tcp_interface.adb @@ -107,9 +107,9 @@ is end if; -- The SMSS is the size of the largest segment that the sender can transmit - Sock.smss := unsigned_short'Min (TCP_DEFAULT_MSS, TCP_MAX_MSS); + Sock.smss := Mss_Size'Min (TCP_DEFAULT_MSS, Mss_Size(TCP_MAX_MSS)); -- The RMSS is the size of the largest segment the receiver is willing to accept - Sock.rmss := unsigned_short(unsigned_long'Min + Sock.rmss := Mss_Size(unsigned_long'Min (unsigned_long(Sock.rxBufferSize), unsigned_long(TCP_MAX_MSS))); @@ -328,9 +328,9 @@ is -- The RMSS is the size of the largest segment the receiver is -- willing to accept - Client_Socket.rmss := unsigned_short'Min + Client_Socket.rmss := Mss_Size(unsigned_short'Min (unsigned_short(Client_Socket.rxBufferSize), - TCP_MAX_MSS); + unsigned_short(TCP_MAX_MSS))); -- Initialize TCP control block Client_Socket.iss := netGetRand; @@ -348,7 +348,7 @@ is Sock.congestState := TCP_CONGEST_STATE_IDLE; -- Initial congestion window Client_Socket.cwnd := unsigned_short(unsigned_long'Min - (unsigned_long(TCP_INITIAL_WINDOW * Client_Socket.smss), + (unsigned_long(TCP_INITIAL_WINDOW * unsigned_short(Client_Socket.smss)), unsigned_long(Client_Socket.txBufferSize))); -- Slow start threshold should be set arbitrarily high Client_Socket.ssthresh := unsigned_short'Last; diff --git a/src/ada/tcp_type.ads b/src/ada/tcp_type.ads index 71139f8..12401f6 100644 --- a/src/ada/tcp_type.ads +++ b/src/ada/tcp_type.ads @@ -59,12 +59,62 @@ package Tcp_Type with SPARK_Mode is 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; + type Mss_Lower_Bound is range 1 .. unsigned_short'Last; + type Mss_Upper_Bound is range 536 .. unsigned_short'Last; - TCP_INITIAL_RTO : constant Systime := 1_000; + -- Mimimum acceptable segment size +#if TCP_MIN_MSS'Defined then + TCP_MIN_MSS : constant Mss_Lower_Bound := $TCP_MIN_MSS; +#else + TCP_MIN_MSS : constant Mss_Lower_Bound := 64; +#end if; + -- Maximum segment size +#if TCP_MAX_MSS'Defined then + TCP_MAX_MSS : constant Mss_Upper_Bound := $TCP_MAX_MSS; +#else + TCP_MAX_MSS : constant Mss_Upper_Bound := 1_430; +#end if; + + type Mss_Size is range 1 .. TCP_MAX_MSS + with Size => unsigned_short'Size; + + -- Default maximum segment size +#if TCP_DEFAULT_MSS'Defined then + TCP_DEFAULT_MSS : constant Mss_Size := $TCP_DEFAULT_MSS; +#else + TCP_DEFAULT_MSS : constant Mss_Size := 536; +#end if; + + subtype Rto_Systime_Max is Systime range 1000 .. Systime'Last; + -- Maximum retransmission timeout +#if TCP_MAX_RTO'Defined then + TCP_MAX_RTO : constant Rto_Systime_Max := $TCP_MAX_RTO; +#else + TCP_MAX_RTO : constant Rto_Systime_Max := 60000; +#end if; + + subtype Rto_Systime is Systime range 100 .. TCP_MAX_RTO; + -- Initial retransmission timeout +#if TCP_INITIAL_RTO'Defined then + TCP_INITIAL_RTO : constant Rto_Systime := $TCP_INITIAL_RTO; +#else + TCP_INITIAL_RTO : constant Rto_Systime := 1000; +#end if; + + -- Minimum retransmission timeout +#if TCP_MIN_RTO'Defined then + TCP_MIN_RTO : constant Rto_Systime := $TCP_MIN_RTO; +#else + TCP_MIN_RTO : constant Rto_Systime := 1000; +#end if; + + -- Size of the congestion window after the three-way handshake is completed +#if TCP_INITIAL_WINDOW'Defined then + TCP_INITIAL_WINDOW : constant unsigned_short := $TCP_INITIAL_WINDOW; +#else TCP_INITIAL_WINDOW : constant unsigned_short := 3; +#end if; -- Override timeout (should be in the range 0.1 to 1 seconds) TCP_OVERRIDE_TIMEOUT : constant Systime := 500; @@ -125,9 +175,11 @@ package Tcp_Type with SPARK_Mode is TCP_FLAG_ACK : constant Tcp_Flags := 16; TCP_FLAG_URG : constant Tcp_Flags := 32; - -- TODO: use preprocessing instead of 14 to be coherent with the C code. - type Chunk_Desc_Array is array (0 .. 14) of Chunk_Desc - with Object_Size => 15 * (32 + System.Word_Size); + type Chunk_Desc_Array_Index is range 0 .. ((TCP_MAX_TX_BUFFER_SIZE + NET_MEM_POOL_BUFFER_SIZE - 1) / NET_MEM_POOL_BUFFER_SIZE); + type Chunk_Desc_Array is array (Chunk_Desc_Array_Index) of Chunk_Desc + with + Object_Size => + (((TCP_MAX_TX_BUFFER_SIZE + NET_MEM_POOL_BUFFER_SIZE - 1) / NET_MEM_POOL_BUFFER_SIZE) + 1) * (32 + System.Word_Size); type Tcp_Tx_Buffer is record chunkCount : unsigned; @@ -135,7 +187,9 @@ package Tcp_Type with SPARK_Mode is chunk : Chunk_Desc_Array; end record with - Convention => C, Object_Size => 64 + 15 * (32 + System.Word_Size); + Convention => C, + Object_Size => + 64 + (((TCP_MAX_TX_BUFFER_SIZE + NET_MEM_POOL_BUFFER_SIZE - 1) / NET_MEM_POOL_BUFFER_SIZE) + 1) * (32 + System.Word_Size); type Tcp_Rx_Buffer is record chunkCount : unsigned; @@ -178,7 +232,7 @@ package Tcp_Type with SPARK_Mode is Src_Port : Port; Dest_Addr : IpAddr; Isn : unsigned; - Mss : unsigned_short; + Mss : Mss_Size; end record with Convention => C;