I never looked at HISTTIMEFORMAT.

If I set HISTTIMEFORMAT, bash captures the time in the history file as what appears to be epoch seconds. This would definitely speed things up.

#1597175957
echo $$
#1597175963
echo $HOME
#1597175967
ls -la
#1597176017
ls
#1597176017
ls
#1597176018
ls
[download]

As you mention, the history file gets written when the shell exits. I too usually have multiple shells at the same time. I guess if we need to separate different sessions we could set HISTFILE to a distinct file name in .bashrc