@pra Nice analysis!
Below is how the reworked CC3000 code handles the issues:
Send Side:May cause more then one TCP packet or not depending on the TI policy for holding a packet before sending.
Receive Side, the driver has a SPARK_ASSERT(data_to_recv <= arraySize(wlan_rx_buffer)); that will panic (send SOS on red LED then AssertionFailure ( 10 blinks) code ) if it ever happens. Never seen one
Endless Loops in CC3000_Spi
There were all kinds of wrong edge detection and races.
All this has been reworked to support the TI IRQ requirements. With read request preemption on a host write. The race to the cc3000 with an unsolicited event v. a Host write. Once the driver is in the idle state, Writes are committed with an atomic CS assertion.
Potential Endless Loop in Evnt_handler
New driver has a timeout mechanism on the even handler. With return to the application with failure codes as per the socket.h API (alal BSD sockets API well almost ;( )
Probable Missed Interrupts
This has been reworked. The DMA is streamlined. The WIF_INT assertion schedules the DMA. On completion of the DMA the buffer is dropped off for consumption by the unsolicited event handler with only the WIF_INT masked. If the unsolicited event handler consume the packet WIF_INT ints are unmasked (the NVIC will assert a CPU IRQ if there was/are a falling edge on the WIF_INT while masked). If it does not the assumption is it was a solicited IRQ as a result of a write. The code handles that as well. None of the WIF_INT masking is an issue because the CC3000 has no queueing, there can be only one outstanding request at a time.
I have posted a pdf of the issues and fixes reported to spark that i made.